Changes between Version 35 and Version 36 of WikiStart


Ignore:
Timestamp:
Jun 18, 2012, 2:00:16 PM (5 years ago)
Author:
mulligan
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v35 v36  
    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.
     6
     7=== CPP 2012 submissions ===
     8
     9Code for the two CerCo CPP 2012 submissions can be found here.  A snapshot of a recent version of Matita for typechecking these submissions can be found here.
    610
    711=== Related work ===