wiki:WikiStart

Version 30 (modified by mulligan, 6 years ago) (diff)

change of title for wilmer

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.

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:

  • On the correctness of an assembler for the MCS-51 microprocessor. Dominic P. Mulligan and Claudio Sacerdoti Coen. Submitted to CPP 2011. Matita formalisation here.
  • Semantics for simple type theory in nominal sets. Murdoch J. Gabbay and Dominic P. Mulligan. Submitted to LFMTP 2011.
  • An executable formalisation of the MCS-51 microprocessor in Matita. Dominic P. Mulligan and Claudio Sacerdoti Coen. Submitted to FMCAD 2011.
  • ​Certifying cost annotations in compilers. Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas and Ronan Saillard. Technical Report, Université Paris Diderot (Paris 7).

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 (44)