Changes between Version 6 and Version 7 of WikiStart


Ignore:
Timestamp:
May 11, 2010, 11:06:26 PM (9 years ago)
Author:
admin
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v6 v7  
    1 = Certified Complexity (CerCo) =
     1= Certified Complexity (!CerCo) =
    22
    3 CerCo (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.
     3!CerCo (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.
    44
    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.