CompCert - Main page

CRANK

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 C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.Get CompCert C »[09/2018] Release of CompCert C version 3.4. It adds more error and warning messages, tightens compatibility with ISO C11, fixes a few bugs, and improves compatibility with newer Coq, Menhir, and OCaml versions.[05/2018] Release of CompCert C version 3.3. It features a source annotation mechanism to tr…