Publications 2009

Academic Journals

  1. Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009.
  2. A. Gotlieb. TCAS software verification using Constraint Programming. The Knowledge Engineering Review, Under revision, 2009.

International Conferences

  1. Frédéric Besson. CPA beats oo-CFA. In Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, Pages 1-6, 2009.
  2. Sandrine Blazy, Benoît Robillard. Live-range Unsplitting for Faster Optimal Coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), Pages 70-79, 2009. download
  3. B. Boyer, T. Genet. Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems. In Proc. of RULE'09, EPTCS, Volume 21, 2009.
  4. David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. In Proc.\ of the 1st NASA Formal Methods Symposium (NFM'09), Pages 111-115, 2009.
  5. Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. In Proc.\ of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), Lecture Notes in Computer Science, Volume 5674, Pages 212-227, 2009.
  6. Delphine Demange, David Sands. All Secrets Great and Small. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP '09, Pages 207-221, Berlin, Heidelberg, 2009.
  7. A. Gotlieb. EUCLIDE: A Constraint-Based Testing platform for critical C programs. In 2th International Conference on Software Testing, Validation and Verification (ICST'09), Denver, CO, 2009.
  8. A. Gotlieb, M. Petit. Towards a Theory for Testing Non-terminating Programs. In 33nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'09), 6 pages, Seattle, USA, 2009.
  9. Gilles Guette, Olivier Heen. A TPM-based Architecture for Improved Security and Anonymity in Vehicular Ad hoc Networks. In In International Vehicular Networking Conference (IEEE VNC 2009), 2009.
  10. Olivier Heen, Gilles Guette, Thomas Genet. On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks. In WISTP 2009 3rd edition, LNCS, Volume 5746, 2009.
  11. Laurent Hubert, David Pichardie. Soundly Handling Static Fields: Issues, Semantics and Analysis. In Proc.\ of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in Theoretical Computer Science, Volume 253, Pages 15-30, 2009.
  12. N. Lazaar, A. Gotlieb, Y. Lebbah. Towards Constraint-Based Local Search for Automatic Test Data Generation. In 1th International Workshop on Search-based Test Data Generation, co-located with ICST 2009, Lillehammer, Norway, 2009.
  13. Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. In Proceedings of the 14th ACM international conference on Functional programming, Pages 287-298, 2009.

Research Reports

  1. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report INRIA, No 0, 2009. download
  2. Tiphaine Turpin, Frédéric Besson, Thomas Jensen. Computing the Least Fix-point Semantics of Logic Programs Using BDDs. Research Report INRIA, No 7107, 2009.


  1. Fré Besson, David Cachera, Thomas Jensen, David Pichardie. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. pp. 223-257, 2009.


  1. Thomas Genet. Reachability Analysis of Rewriting for Software Verification. Habilitation à diriger des recherches Université de Rennes 1, 2009.