BACK TO INDEX

Publications of year 1999

Thesis

  1. Thomas Jensen. Analyse statiques de programmes : fondements et applications. document d'habilitation à diriger des recherches, Université de Rennes 1, décembre 1999. 
    @PhDThesis{Jensen:99:Hab,
Author={Thomas Jensen},
Title={Analyse statiques de programmes : fondements et applications},
School = {Université de Rennes 1},
Type = "document d'habilitation à diriger des recherches",
Month={décembre},
Year={1999}
}


  2. T. Thorn. Vérification de politiques de sécurité par analyse de programmes. PhD thesis, Université de Rennes I, Ifsic, Irisa, février 1999. 
    @PHDTHESIS{TT99,
author = {T. Thorn},
school = {Université de Rennes I, Ifsic, Irisa},
title = {Vérification de politiques de sécurité par analyse de programmes},
MONTH = {février},
year = {1999},

}


Conference articles

  1. F. Besson, T. Jensen, and J.P. Talpin. Polyhedral Analysis for Synchronous Languages. In Gilberto Filé, editor, International Static Analysis Symposium, SAS'99, volume 1694 of Lecture Notes in Computer Science, September 1999. Springer-Verlag. Keyword(s): synchronous languages, abstract interpretation, reachability analysis, infinite state systems.
    We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of a reactive system. A distinguished feature of the analysis is that it is expressed and proved correct with respect to the source program rather than on an intermediate representation of the program. The analysis calculates a safe approximation to the set of reachable states by a symbolic fixed point computation in the domain of convex polyhedra using a novel widening operator based on the convex hull representation of polyhedra.

    @INPROCEEDINGS{SAS99:BJT,
AUTHOR= "F. Besson and T. Jensen and J.P. Talpin",
TITLE= "{P}olyhedral {A}nalysis for {S}ynchronous {L}anguages",
EDITOR = {Gilberto Filé},
PUBLISHER = {Springer-Verlag},
YEAR = {1999},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1694},
BOOKTITLE={International Static Analysis Symposium, SAS'99},
MONTH={September},
keywords={synchronous languages, abstract interpretation, reachability analysis, infinite state systems},
abstract={We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of a reactive system. A distinguished feature of the analysis is that it is expressed and proved correct with respect to the source program rather than on an intermediate representation of the program. The analysis calculates a safe approximation to the set of reachable states by a symbolic fixed point computation in the domain of convex polyhedra using a novel widening operator based on the convex hull representation of polyhedra.} 
}


  2. T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security properties. In Proc. of the 20th IEEE Symp. on Security and Privacy, pages 89-103, mai 1999. New York: IEEE Computer Society. 
    @InProceedings{SSP99,
author = {T. Jensen and D. Le~Métayer and T. Thorn},
title = {Verification of control flow based security properties},
booktitle = {Proc.\ of the 20th IEEE Symp.~on Security and Privacy},
year = {1999},
pages = {89--103},
publisher = {New York:\ IEEE Computer Society},
month = {mai} 
}


Miscellaneous

  1. E. Denney, P. Fradet, C. Goire, T. Jensen, and D. Le Métayer. Procédé de vérification de transformateurs de codes pour un système embarqué, notamment sur une carte à puce, juillet 1999. Note: Brevet d'invention. 
    @misc{brevet99,
author = {E. Denney and P. Fradet and C. Goire and T. Jensen and D. Le~Métayer},
title = {Procédé de vérification de transformateurs de codes pour un système embarqué, notamment sur une carte à puce},
Year={1999},
Note = {Brevet d'invention},
Month={juillet}
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html