This page gathers the publications that have been made in the context of the project.

International

Articles

Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning. 43(3), pp. 263-288, October 2009 pdf
Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. Journal of Symbolic Computation. 45(11), pp 1184-1211, November 2010.
Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 2011.
Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto. Functional Dependencies of C Functions via Weakest Pre-Conditions. International Journal for Software Tools for Technology Transfer (STTT), octobre 2011. More information
Jean-Christophe Filliâtre. Deductive software verification. International Journal on Software Tools for Technology Transfer (STTT), 13(5):397-403, August 2011.

Books

Bernhard Beckert and Claude Marché, dir. Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Paris, France. June 2010. pdf

Conferences

Pascal Cuoq and Julien Signoles. Experience Report: OCaml for an industrial-strength static analysis framework. 14th ACM SIGPLAN International Conference on Functional Programming. Edinburgh, Scotland. September 2009. pdf
Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In 37th symposium Principles of Programming Languages, pages 83-92. ACM Press, January 2010. pdf
Silvain Rideau and Xavier Leroy. Validating register allocation and spilling. In Compiler Construction (CC 2010), volume 6011 of Lecture Notes in Computer Science, pages 224-243. Springer, March 2010. pdf
Sandrine Blazy, Benoît Robillard and Andrew Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. In European Symposium On Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 145-164. Springer, March 2010. pdf
David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien Signoles. Taster, a Frama-C plugin to enforce Coding Standards. Présenté à ERTS, Toulouse, France. May 2010. pdf
Asma Tafat, Sylvain Boulmé, and Claude Marché. A refinement methodology for object-oriented programs. In Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, pages 143-159, Paris, France. June 2010. pdf
Dillon Pariente and Emmanuel Ledinot, Formal Verification of Industrial C Code using Frama-C: a Case Study. In Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Paris, France. June 2010.
Ali Ayad and Claude Marché. Multi-prover verification of floating-point programs. In Jürgen Giesl and Reiner Hähnle, editors. Fifth International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, Edinburgh, Scotland. July 2010. pdf
Paolo Herms. Certification of a chain for deductive program verification. In Yves Bertot, editor, 2nd Coq Workshop, satellite of ITP'10, 2010. pdf
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy. Formal verification of object layout for C++ multiple inheritance. In 38th symposium on Principles of Programming Languages (POPL 2011), January 2011. pdf
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Towards Optimizing Certified Compilation in Flight Control Software. In Workshop on Predictability and Performance in Embedded Systems (PPES 2011), March 2011. pdf
Jean-Christophe Filliâtre and K. Kalyanasundaram. Functory: A Distributed Computing Libraryfor Objective Caml. In Trends in Functional Programming, Madrid, Spain, May 2011
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, Aout 2011.
Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, Lecture Notes in Computer Science. Springer, December 2011.
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy. A mechanized semantics for C++ object construction and destruction, with applications to resource management. In 39th symposium on Principles of Programming Languages, ACM Press, January 2012, Philadelphie, PA, USA.
Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel and Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS 2012), February 2012, Toulouse, France.

National

Articles

Julien Signoles. Foncteurs impératifs et composés : la notion de projets dans Frama-C. Studia Informatica Universalis. 2009. pdf
Julien Signoles. Une bibliothèque de typage dynamique en OCaml. Studia Informatica Universalis. 2011

Conferences

Richard Bonichon and Pascal Cuoq. Une table d'association d'intervalles fusionnable. Actes des Journées Francophones des Langages Applicatifs. La Ciotat. January 2010. pdf
Jean-Christophe Filliâtre and Krishnamani Kalyanasundaram. Une bibliothèque de calcul distribué pour Objective Caml. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA.

Research Reports

K. Kalyanasundaram and Claude Marché. Automated generation of loop invariants using predicate abstraction. Research Report 7714, INRIA, August 2011. pdf

Dissemination Actions

Popularization Articles

Xavier Leroy. Comment faire confiance à un compilateur? La Recherche, 440, April 2010. pdf

Popularization Conferences

Xavier Leroy, "Une introduction à la vérification formelle de codes critiques". Exposé à la journée de rencontre INRIA-industrie "Modélisation et systèmes sûrs", Toulouse, May 2010. pdf
Pascal Cuoq, Damien Doligez and Julien Signoles, Lightweight Typed Customizable Unmarshaling, ML Workshop 2011, Tokyo, September 2011.

Misc

Poster at the System@TIC Symposium, Châtenay-Malabry, June 2009.
Poster at the Grand Colloque STIC, Paris, January 2010.
Poster at the System@TIC symposium, Paris, June 2010.