wiki:WikiStart

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

--

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.

Potential outlets for publicaton

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

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)