Changes between Version 4 and Version 5 of WikiStart


Ignore:
Timestamp:
May 11, 2010, 10:53:16 PM (9 years ago)
Author:
admin
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v4 v5  
    11= Certified Complexity (CerCo) =
    2 == EU FP7 Collaborative (FET Open) Project 243881 ==
    32
    4 === Abstract ===
     3CerCo (Certified Complexity) is a European research project in the [http://cordis.europa.eu/fp7/home_en.html 7th Research Framework Programme] (FP7) of the [http://ec.europa.eu/index_en.htm European Commission] (project number 243381). The project is situated in the FP7 theme [http://cordis.europa.eu/fp7/ict/ssai/home_en.html 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.
     4
    55The 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.
    66