CerCo: A cost annotating compiler for C

Presentation

The project aims to the construction of a formally verified complexity preserving compiler from a large subset of C to some typical microcontroller assembly, of the kind traditionally used in embedded systems. The work comprise the definition of cost models for the input and target languages, and the machine-checked proof of preservation of complexity (concrete, not asymptotic) along compilation. The compiler will also return tight and certified cost annotations for the source program, providing a reliable infrastructure to draw temporal assertions on the executable code while reasoning on the source. The compiler will be open source, and all proofs will be public domain.

Papers

Distribution

You can download the source distribution, following these links:

• acc-0.2.tar.gz : The cost annotating C compiler (untrusted prototype).

• cost-plugin-0.1.tar.gz : The frama-C plugin. (It needs the compiler to be installed, as well as Frama-C Nitrogen.)

• lamcost-0.2.tar.gz : A cost annotating compiler for MiniML.

If you are in a hurry, we have made a script that builds an automatic local installation of our software and all its dependencies. (You just need a standard gcc installation.)

• cerco-software.sh

Web applications

You can test our cost annotating compilers directly in your web browser by following this link:

• CerCo C compiler
• MiniML compiler

Mechanically checked proofs for a toy CerCo compiler

Most of the formal proofs have been done in the Coq proof assistant. The following link is an online documentation of the development:

• Coq proof development

Related links

• The webpage of the european project CerCo .