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.