News archive

[07/2018] Award: I am honored to receive the Grand prix Inria - Académie des sciences 2018.

[01/2018] Publication: CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler, by Daniel Kästner et al, presented at ERTS 2018. This paper describes the first use of CompCert in production for a safety-critical application in the nuclear industry, including IEC 60880 certification.

[12/2017] I was interviewed by Jean Yang as part of a "People of Programming Languages" series.

[06/2017] Publication: A Formally Verified Compiler for Lustre, by Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, myself, Marc Pouzet and Lionel Rieg, PLDI 2017.

[02/2017] Software and Coq development: version 3.0 of Compcert is released. This is the first CompCert version that fully supports 64-bit target processors; more precisely, pointers and memory addresses are no longer assumed to be 32-bit wide and can be 64-bit wide as well depending on the target. Definitely 3.0 material!

[11/2016] Public lecture: video of my Milner award lecture at the Royal Society.

[11/2016] Award: I am deeply honored to receive one of the two 2016 van Wijngaarden awards from CWI.

[01/2016] Award: my POPL 2006 paper, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, received the ACM SIGPLAN Most Influential POPL Paper Award.

[12/2015] Award: I am proud to become a Fellow of the ACM.

[07/2015] Award: I am deeply honored to receive the 2016 Royal Society Milner Award.

[10/2014] Publication: A formally-verified C static analyzer, with Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, and David Pichardie, POPL 2015.

[10/2014] Publication: Verified compilation of floating-point computations, with Sylvie Boldo, Jacques-Henri Jourdan, and Guillaume Melquiond, Journal of Automated Reasoning 54(2).

[09/2014] Software and Coq development: version 2.4 of Compcert is released, featuring a revised handling of single-precision floating-point computations.

[06/2014] Conference: I have the pleasure of co-chairing the program committee of CPP 2015, with Alwen Tiu. CPP is the conference on Certified Programs and Proofs, and is for the first time colocated with POPL 2015 in Mumbai, India. Consider submitting!

[05/2014] Software and Coq development: release of Compcert version 2.3, integrating Jacques-Henri Jourdan's formally-verified parser.

[04/2014] Book chapter: Andrew Appel's book Program Logics for Certified Compilers is published. It contains much material about CompCert, including a chapter on the CompCert memory model written by Andrew Appel, Sandrine Blazy, Gordon Stewart and I.

[02/2014] Software and Coq development: release of Compcert version 2.2, with two new static analyses (value analysis and need analysis) that enable more optimizations.

[06/2013] Software and Coq development: version 2.0 of the Compcert C verified compiler is released. It features the long-awaited support for 64-bit integers, as well as a new register allocator -- decidedly "2.0" material!

[01/2013] Software and Coq development: release of version 1.12 of the Compcert C verified compiler.

[01/2013] Publication: A Formally-Verified C Compiler Supporting Floating-Point Arithmetic, with Sylvie Boldo, Jacques-Henri Jourdan, and Guillaume Melquiond, 21st IEEE ARITH conference, April 2013.

[12/2012] Award: I am deeply honored to receive the Microsoft Research Verified Software Milestone Award in recognition of my work on CompCert.

[10/2012] Publication: A formally-verified alias analysis, with Valentin Robert, conference CPP 2012.

[07/2012] Software and Coq development: release of version 1.11 of the Compcert C verified compiler. Now with a fully-verified handling of floating-point arithmetic. (See paper above).

[06/2012] Tech report: The CompCert memory model, version 2, with Andrew Appel, Sandrine Blazy, and Gordon Stewart, INRIA research report RR-7987. Everything you (n)ever wanted to know about recent evolutions of the CompCert memory model.

[03/2012] Software and Coq development: release of version 1.10 of the Compcert C verified compiler.

[01/2012] Publication: Validating LR(1) parsers, with Jacques-Henri Jourdan and François Pottier, symposium ESOP 2012.

[12/2011] Publication: Formally verified optimizing compilation in ACG-based flight control software, with Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Marc Pantel and Jean Souyris, symposium ERTS2 2012.

[11/2011] Publication: A mechanized semantics for C++ object construction and destruction, with applications to resource management, with Tahina Ramananandro and Gabriel Dos Reis. POPL 2012.

[10/2011] Award: along with Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan, I received the 2011 La Recherche award in Information Sciences for our work on the CompCert verified C compiler.

[08/2011] Software and Coq development: release of version 1.9 of the Compcert C verified compiler.

[06/2011] Course material: Proving a compiler: mechanized verification of program transformations and static analyses, lecture given at the Oregon Programming Languages Summer School 2011

[04/2011] Publication: A list-machine benchmark for mechanized metatheory, with Andrew Appel and Robert Dockins, to appear in Journal of Automated Reasoning.

[01/2011] Publication: Towards optimizing certified compilation in flight control software, with Ricardo Bedin França, Denis Favre-Felix, Marc Pantel and Jean Souyris, workshop PPES 2011.

[11/2010] Publication: Formal verification of object layout for C++ multiple inheritance, with Tahina Ramananandro and Gabriel Dos Reis, POPL 2011.

[09/2010] Software and Coq development: release of version 1.8 of the Compcert C verified compiler.

[04/2010] Popular science: Comment faire confiance à un compilateur? (in French). A short introduction to compiler verification, published in the French magazine La Recherche, april 2010 issue.

[03/2010] Software and Coq development: release of version 1.7 of the Compcert C verified compiler, featuring a new C type-checker/elaborator/simplifier and a refined memory model.

[12/2009] Publication: Validating register allocation and spilling, with Silvain Rideau, Compiler Construction 2010.

[12/2009] Publication: A verified framework for higher-order uncurrying optimizations, with Zaynah Dargaye, Higher-Order and Symbolic Computation 22(3).

[11/2009] Publication: A formally verified compiler back-end. My ars magna on the Compcert verified back-end (80 pages!), now published in Journal of Automated Reasoning 43(4).

[11/2009] Publication: A simple, verified validator for software pipelining, with Jean-Baptiste Tristan, POPL 2010.

[08/2009] Course material: Mechanized semantics, with applications to program proof and compiler verification, lecture given at the 2009 Marktoberdorf summer school.

[08/2009] Software and Coq development: release of version 1.5 of the Compcert C verified compiler. Now with full support for goto statements!

[07/2009] Nostalgia: the books Le langage Caml (1993; 1999) and Manuel de référence du langage Caml (1993) are now freely available in PDF format.

[04/2009] Publication: Formal verification of a realistic compiler. A short overview of the CompCert verified compiler, published in Communications of the ACM, July 2009, along with a perspective written by Greg Morrisett.

[04/2009] Software and Coq development: release of version 1.4 of the Compcert C verified compiler.

[03/2009] Publication: Verified validation of Lazy Code Motion, with Jean-Baptiste Tristan, PLDI 2009.

[02/2009] Publication: Compilation of extended recursion in call-by-value functional languages, with Tom Hirschowitz and J. B. Wells, published in Higher-Order and Symbolic Computation 22(1).

[01/2009] Publication: Mechanized semantics for the Clight subset of the C language, with Sandrine Blazy, published in Journal of Automated Reasoning 43(3).

[12/2008] Software: release of Objective Caml version 3.11.

[08/2008] Software and Coq development: release of version 1.3 of the Compcert C verified compiler.

[03/2008] Software and Coq development: first public release of the Compcert C verified compiler.

[02/2008] Publication: Formal verification of a C-like memory model and its uses for verifying program transformations, with Sandrine Blazy, published in Journal of Automated Reasoning 41(1). Accompanied with a Coq development.

[02/2008] Talk: Du langage à l'action: compilation et typage (in French), tutorial lecture given at Collège de France in Gérard Berry's course. A video of the lecture is available.

[12/2007] Publication: Coinductive big-step operational semantics, with Hervé Grall, published in Information and Computation. Accompanied with a Coq development.

[12/2007] Publication: Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves, with Laurence Rideau and Bernard Paul Serpette, published in Journal of Automated Reasoning. Accompanied with a Coq development.

[11/2007] Publication: Formal verification of translation validators: A case study on instruction scheduling optimizations, with Jean-Baptiste Tristan, POPL 2008.

[10/2007] Award: I am honored to be awarded the 2007 Michel Monpetit prize of the French Academy of Sciences.

[07/2007] Publication: Mechanized verification of CPS transformations, with Zaynah Dargaye, LPAR 2007.

[06/2007] Event: A colloquium in honor of Gérard Huet, in Paris, June 22-23, 2007.

[01/2007] Technical report and Coq development: A solution to the POPLmark challenge, based on a locally nameless representation of terms in the style of McKinna and Pollack.

[08/2006] Publication: Formal verification of a C compiler front-end, with Sandrine Blazy and Zaynah Dargaye. Proceedings of Formal Methods 2006, LNCS 4085.

[03/2006] Publication: Coinductive big-step operational semantics. Proceedings of ESOP 2006, LNCS 3924. Accompanying Coq development: (1) semantics.v; (2) typing.v; (3) compilation.v.

[01/2006] Publication: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of POPL 2006.