BACK TO INDEX

Publications of year 2002

Thesis

  1. F. Besson. Analyse modulaire de programmes. PhD thesis, Université de Rennes 1, 2002. [WWW] 
    @PhDThesis{Besson:02:PhD,
author = {F. Besson},
title = {Analyse modulaire de programmes},
school = {Université de Rennes 1},
year = 2002,
url = {http://www.irisa.fr/lande/fbesson/fbesson.html} 
}


  2. Siegfried Rouvrais. Utilisation d'agents mobiles pour la construction de services distribués. PhD thesis, Université de Rennes 1, juillet 2002. Note: N. d'ordre : 2614. 
    @phdthesis{Rouvrais02a,
author={Siegfried Rouvrais},
year = {2002},
school = {Université de Rennes~1},
note = {N. d'ordre~: 2614},
title = {Utilisation d'agents mobiles pour la construction de services distribués},
month = {juillet} 
}


Articles in journal or book chapters

  1. T. Jensen. Types in program analysis. In Torben Mogensen, David Schmidt, and I. Hal Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, Lecture Notes in Computer Science 2566, pages 204-222. Springer-Verlag, 2002. 
    @incollection{Jensen:02:Types,
title = {Types in program analysis},
author = {T. Jensen},
editor = {Torben Mogensen and David Schmidt and I. Hal Sudborough},
booktitle = {The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science 2566},
YEAR = {2002},
pages = "204--222" 
}


  2. E. Denney and T. Jensen. Correctness of Java Card method lookup via logical relations. Theoretical Computer Science, 283:305-331, 2002. 
    @Article{Denney:02:Correctness,
author = "E. Denney and T. Jensen",
title = "Correctness of {J}ava {C}ard method lookup via logical relations",
journal = "Theoretical Computer Science",
year = "2002",
volume = "283",
pages = "305--331" 
}


Conference articles

  1. F. Besson, Thomas de Grenier de Latour, and T. Jensen. Secure calling contexts for stack inspection. In Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002), pages 76-87, 2002. ACM Press. [WWW]
    Stack inspection is a mechanism for programming secure applications by which a method can obtain information from the call stack about the code that (directly or indirectly) invoked it. This mechanism plays a fundamental role in the security architecture of Java and the .NET Common Language Runtime. A central problem with stack inspection is to determine to what extent the local checks inserted into the code are sufficient to guarantee that a global security property is enforced. In this paper, we present a technique for inferring a secure calling context for a method. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. This is particularly useful for annotating library code in order to avoid having to re-analyse libraries for every new application. The technique is a constraint based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.

    @InProceedings{Besson:02:CallingContexts,
author = {F. Besson and Thomas de~Grenier~de~Latour and T. Jensen},
title = {Secure calling contexts for stack inspection},
booktitle = {Proc.~of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002)},
year = {2002},
publisher = {ACM Press},
pages = "76--87",
url = {http://www.irisa.fr/lande/fbesson/fbesson.html},
abstract = {Stack inspection is a mechanism for programming secure applications by which a method can obtain information from the call stack about the code that (directly or indirectly) invoked it. This mechanism plays a fundamental role in the security architecture of Java and the .NET Common Language Runtime. A central problem with stack inspection is to determine to what extent the local checks inserted into the code are sufficient to guarantee that a global security property is enforced. In this paper, we present a technique for inferring a secure calling context for a method. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. This is particularly useful for annotating library code in order to avoid having to re-analyse libraries for every new application. The technique is a constraint based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.} 
}


  2. Thomas Jensen, Florimond Ployette, and Olivier Ridoux. Iteration schemes for fixed point conputation. In A. Ingolfsdottir and Z. Esik, editors, Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02), pages 69-76, 2002. 
    @InProceedings{Jensen:02:Iteration,
author = {Thomas Jensen and Florimond Ployette and Olivier Ridoux},
title = {Iteration schemes for fixed point conputation},
booktitle = {Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02)},
year = "2002",
editor = {A.~Ingolfsdottir and Z.~Esik},
pages = {69--76},

}


  3. Marc Éluard and Thomas Jensen. Secure object flow analysis for Java Card. In Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02), 2002. IFIP/USENIX. 
    @InProceedings{Eluard:02:SecureObjectFlow,
author = {Marc Éluard and Thomas Jensen},
title = {Secure object flow analysis for Java Card},
booktitle = {Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02)},
year = {2002},
OPTeditor = {P.~Honeyman},
organization = {IFIP/USENIX},

}


Internal reports

  1. T. Genet and V. Viet Triem Tong. Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation. Technical report RR-4576, INRIA, 2002. [WWW] Keyword(s): Equational theories, proof by induction, abstract interpretation, rewriting.
    In this paper we present a method to prove automatically initial negative properties on equational specifications. This method tends to combine induction and abstract interpretation. Induction is performed in a classical way using cover sets. Abstract interpretation is done using an additional set of equations used to approximate the initial model into an abstract one. Like in the methods dedicated to the proof by induction of positive properties, the equational specification is supposed to be oriented into a terminating, confluent and complete term rewriting system.

    @TECHREPORT{GenetVTTong-RR02,
AUTHOR = "Genet, T. and Viet Triem Tong, V.",
TITLE = "{P}roving {N}egative {C}onjectures on {E}quational {T}heories using {I}nduction and {A}bstract {I}nterpretation",
INSTITUTION = {INRIA},
NUMBER = {RR-4576},
YEAR = 2002,
KEYWORDS = {Equational theories, proof by induction, abstract interpretation, rewriting},
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-inria02.ps.gz},
ABSTRACT= {In this paper we present a method to prove automatically initial negative properties on equational specifications. This method tends to combine induction and abstract interpretation. Induction is performed in a classical way using cover sets. Abstract interpretation is done using an additional set of equations used to approximate the initial model into an abstract one. Like in the methods dedicated to the proof by induction of positive properties, the equational specification is supposed to be oriented into a terminating, confluent and complete term rewriting system.} 
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html