Changes between Version 5 and Version 6 of WikiStart


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

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v5 v6  
    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=== Learn More ===
     8 1. Concept and Objectives, progress beyond state-of-the-art, S/T methodology and work plan
     9   1. [wiki:Proposal1.1 Concept and project objective(s)]
     10   2. [wiki:Proposal1.2 Progress beyond state of the art]
     11   3. [wiki:Proposal1.3 S/T methodology and associated work plan]
     12 2. Implementation
     13   1. [wiki:Proposal2.1 Management structure and procedures]
     14   2. [wiki:Proposal2.2 Beneficiaries]
     15   3. [wiki:Proposal2.3 Consortium as a whole]
     16   4. [wiki:Proposal 2.4 Resources to be committed]
     17 3. Potential impact
     18   1. [wiki:Proposal3.1 Strategic impact]
     19   2. [wiki:Proposal3.2 Plan for the use and dissemination of foreground]
    620
    721=== Members ===