The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs.

Between december 2005 and december 2008, this project was funded by ANR (grant number ANR-05-SSIA-0019), as part of the ARA SSIA programme. Since 2009, we are continuing the CompCert investigations, in part within the projects U3CAT (ANR Arpege, 2009-2011), ASCERT (FNRAE, 2009-2011), and Hisseo (Digiteo, 2008-2010).

News

[03/2011] Release of version 1.8.1 of the Compcert C compiler. Now compatible with Coq 8.3pl1, and including algorithmic improvements (lower compilation times) and better handling of initialized global variables.

[09/2010] Version 1.8 of the Compcert C compiler is available. It includes a larger subset of C (including side-effects within expressions) as its source language; a new port generating x86-32 bits code; and more precise semantics for volatile accesses.

[03/2010] Release of version 1.7 of the Compcert C compiler, featuring a new C type-checker/elaborator/simplifier and a refined memory model.

[01/2010] Release of version 1.6 of the Compcert C compiler.

[11/2009] Publication: A formally verified compiler back-end. An extensive (80 pages!) description of the back-end part of Compcert, published in Journal of Automated Reasoning 43(4).

[08/2009] Release of version 1.5 of the Compcert C compiler. Now with full support for goto statements!

[07/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.

[06/2009] Release of version 1.4.1 of the Compcert C compiler. (This version is functionally identical to version 1.4, but compatible with Coq 8.2-1.)

[04/2009] Release of version 1.4 of the Compcert C compiler.

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

[08/2008] Release of version 1.3 of the Compcert C compiler.

[03/2008] First public release (version 1.2) of the Compcert C compiler.

[02/2008] Creation of this Web site.