Publications 2009
Academic Journals
- Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009.
- A. Gotlieb. TCAS software verification using Constraint Programming. The Knowledge Engineering Review, Under revision, 2009.
International Conferences
- 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.
- 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
- B. Boyer, T. Genet. Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems. In Proc. of RULE'09, EPTCS, Volume 21, 2009.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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
- Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report INRIA, No 0, 2009. download
- 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.
Misc
- 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.
Thesis
- Thomas Genet. Reachability Analysis of Rewriting for Software Verification. Habilitation à diriger des recherches Université de Rennes 1, 2009.