Changes between Version 38 and Version 39 of WikiStart


Ignore:
Timestamp:
Jan 11, 2013, 4:08:59 PM (6 years ago)
Author:
campbell
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v38 v39  
    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== !CerCo workshops ==
     8
     9There are two upcoming workshops featuring results from the !CerCo project:
     10
     11 * [wiki:HiPEAC13 The CerCo workshop at HiPEAC'13], Wednesday 23rd January in the afternoon.
     12 * [http://cerco.cs.unibo.it/innovative_techniques_on_timing_analysis_technical_day/ The Technical Day on Innovative Techniques on Timing Analysis] at ETAPS'13 on March 23rd, held jointly with the PROARTIS project.
    613
    714=== CPP 2012 submissions ===