Compcert
Encyclopedia
CompCert is a formally verified
optimizing compiler
for a subset of the C programming language which currently targets PowerPC
, ARM
and 32-bit x86 architectures. This project, led by Xavier Leroy
, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proved in Coq
. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of gcc (version 3) at optimization level -O1, and always better than that of gcc without optimizations.
According to Andrew Appel
, "Part of Leroy’s achievement is that he makes it look like it's not so difficult after all: now that he's found the right architecture for building verified compilers, everyone will know how to do it."
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
optimizing compiler
Compiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
for a subset of the C programming language which currently targets PowerPC
PowerPC
PowerPC is a RISC architecture created by the 1991 Apple–IBM–Motorola alliance, known as AIM...
, ARM
ARM
An arm is an upper limb of the body.Arm may also refer to:-Geography:* Arm , a narrow stretch of a larger body of water** Canal arm, a subsidiary branch of a canal or inland waterway** Distributary or arm, a subsidiary branch of a river...
and 32-bit x86 architectures. This project, led by Xavier Leroy
Xavier Leroy
Xavier Leroy is a French computer scientist and programmer. He is best known for his role as a primary developer of the Objective Caml system...
, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proved in Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of gcc (version 3) at optimization level -O1, and always better than that of gcc without optimizations.
According to Andrew Appel
Andrew Appel
Andrew Wilson Appel is the Eugene Higgins Professor of computer science at Princeton University, New Jersey. He is especially well-known because of his compiler books, the Modern Compiler Implementation in ML series, as well as Compiling With Continuations...
, "Part of Leroy’s achievement is that he makes it look like it's not so difficult after all: now that he's found the right architecture for building verified compilers, everyone will know how to do it."