Certified Complexity (CerCo)

CerCo (Certified Complexity) is a European research project in the  7th Research Framework Programme (FP7) of the  European Commission (project number 243381). The project is situated in the FP7 theme  Information & Communication Technologies (ICT) in the topic Future and Emerging Technologies (FET Open). The project has started February 1st, 2010, and will have a duration of 3 years.

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.

Software

CerCo's Live CD

Try out CerCo's Live CD: http://cerco.cs.unibo.it/livecd/binary.hybrid.iso You can boot your machine with the Live CD or you can emulate it using a virtual machine (virtualbox reccommended). Once logged in, you can try the Frama-C Cost Annotating Compiler by running "cerco -ide filename.c" or you can browse the certification of the CerCo compiler by running "matita" and exploring the source code in the cerco/src directory.

Debian Packages for the CerCo Software

Tired of the Live CD? We provide Debian packages for all the software developed in CerCo and its dependencies.

Source code

Source code is provided as well.

CerCo workshops

We held two workshops in 2013 featuring results from the CerCo project:

CPP 2012 submissions

Code for the two CerCo? CPP 2012 submissions can be found attached to the bottom of this page in the file "CPP2012.tar.gz". A snapshot of a recent version of Matita for typechecking these submissions can also be found attached in the file "Matita-18-06-2012.tar.gz". To build Matita, extract the files, change to the target directory, type ./configure and then make world. An optimised set of Matita binaries (matita.opt) will be built in the "matita" subdirectory.

Related work

A collection of links to work similar to CerCo can be found here.

Potential outlets for publicaton

A list of potential workshops, conferences and journals suitable for CerCo publications can be found here.

Publications

Publications that fall under the aegis of the CerCo project:

Systems (QAPL 2013), Rome, 23rd‐24th March 2013, Electronic Proceedings in Theoretical Computer Science, 2013

Learn More

  1. Concept and Objectives, progress beyond state-of-the-art, S/T methodology and work plan
    1. Concept and project objective(s)
    2. Progress beyond state of the art
    3. S/T methodology and associated work plan
  2. Implementation
    1. Management structure and procedures
    2. Beneficiaries
    3. Consortium as a whole
    4. Resources to be committed
  3. Potential impact
    1. Strategic impact
    2. Plan for the use and dissemination of foreground

Deliverables

Members

 University of Bologna (coordinator)

 University of Edinburgh

 Université Paris Diderot

Attachments