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.

The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the ISO C90 / ANSI C language, generating efficient code for the PowerPC, ARM and x86 processors. Get CompCert C »

The CompCert project is funded by ANR (grants ANR-05-SSIA-0019, ANR-08-SEGI-021, ANR-11-INSE-003) with additional support from FNRAE and Digiteo. See the list of partners for more information.

Diagram of the CompCert compiler

News

[06/2015] Release of CompCert C version 2.5. Novelties include a formally-verified type checker for CompCert C, a more careful modeling of pointer comparisons against the null pointer, algorithmic improvements in the handling of deeply nested struct and union types, much better ABI compatibility for passing composite values, support for GCC-style extended inline asm, and more complete generation of DWARF debugging information (contributed by AbsInt).

[09/2014] The working sources for CompCert are now hosted on Github.

[09/2014] CompCert C version 2.4 is released, with a revised handling of single-precision floating-point arithmetic and support for C99 compound literals and switch statements over 64-bit integers.

[06/2014] As part of a licensing agreement with Inria, AbsInt Angewandte Informatik GmbH will market and provide support for the CompCert verified C compiler.

[05/2014] CompCert C version 2.3 is released. Novelties includes a formally-verified parser, and support for C99 designated initializers.

[02/2014] Release of CompCert C version 2.2, featuring more aggressive optimizations, support for more features of ISO C99 (especially variable-argument functions), and improved conformance with the target ABIs.

[10/2013] Minor release of CompCert C version 2.1. The main novelty is support for the _Alignas attribute from ISO C2011, for finer control of alignment.

[06/2013] CompCert C version 2.0 is now available, featuring two major improvements: 1- support for 64-bit integer arithmetic (type long long) and 2- a new register allocator based on a posteriori validation.

[03/2013] Release of version 1.13 of the CompCert C compiler. The semantics of pointers "one past the end of an array" is now properly defined as in the ISO C standard.

[01/2013] CompCert C versions 1.12 and 1.12.1 are released. The two versions are functionally identical, but 1.12 is for Coq 8.3 and 1.12.1 for Coq 8.4.

[12/2012] The Microsoft Research Verified Software Milestone Award was awarded to Xavier Leroy for his work on the CompCert verified compiler.

[07/2012] CompCert C version 1.11 is released. Novelties include a full formalization and proof of floating-point arithmetic, and performance improvements: function inlining, more aggressive constant propagation and CSE.

[06/2012] A technical report describing the memory model used in CompCert versions 1.7 and up.

[03/2012] Release of version 1.10 of the CompCert C compiler. Now with a provably-correct implementation of volatile accesses and by-value structure passing and assignment, plus various small performance improvements, and a user's manual.

[02/2012] 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] Release of version 1.9.1 of the Compcert C compiler.

[10/2011] The 2011 La Recherche prize in Information Sciences was awarded to Xavier Leroy, Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan for their work on the CompCert verified C compiler.

[08/2011] Release of version 1.9 of the Compcert C compiler. Novelties include a reference C interpreter and stronger semantic preservation results.

[05/2011] Release of version 1.8.2 of the Compcert C compiler.

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