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.

This project is funded by ANR (grant number ANR-05-SSIA-0019), as part of the ARA SSIA programme (2005-2008).

News

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

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