Changes between Version 47 and Version 48 of WikiStart

May 14, 2013, 6:33:00 PM (4 years ago)



  • WikiStart

    v47 v48  
    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.
    7 == !CerCo's Live CD ==
     7== Software ==
     9=== !CerCo's Live CD ===
    911Try out !CerCo's Live CD: []
    1315by running "matita" and exploring the source code in the cerco/src directory.
    15 == Debian Packages for the !CerCo Software ==
     17=== Debian Packages for the !CerCo Software ===
    1719Tired of the Live CD? We provide Debian packages for all the software developed in !CerCo and its dependencies.
    3133 * raw-attachment:matita_0.99.2-1_amd64.deb
    3234   A version of Matita that can process the !CerCo certification of the Trusted !CerCo Cost Annotating Compiler
     37=== Source code ===
     39Source code is provided as well.
     41 * raw-attachment:acc_0.2.orig.tar.gz !CerCo Cost Annotating Compiler
     42 * raw-attachment:acc-trusted_0.2.orig.tar.gz Trusted !CerCo Cost Annotating Compiler
     43 * raw-attachment:certification_20130430.tgz Matita source code of the formal correctness proof
     44 * raw-attachment:cost-plug-in_0.2.orig.tar.gz !CerCo's Frama-C Cost Plugin
    3446== !CerCo workshops ==
    7688=== Deliverables ===
    77  * D2.1 Compiler design and intermediate languages: raw-attachment:D2_1.pdf
     89 * D2.1 Compiler design and intermediate languages: raw-attachment:D2-1-addendum.pdf
    7890 * D2.2 Prototype implementation: raw-attachment:D2_2.pdf
    7991 * D3.1 Executable formal semantics of C: raw-attachment:D3_1.pdf
    8092 * D4.1 Executable formal semantics of machine code: raw-attachment:D4_1.pdf raw-attachment:D4_1_Code.tar.gz
     93 * D4.2 CIC encoding: Back-end: raw-attachment:D4_2.pdf
     94 * D4.3 Executable formal semantics of back-end intermediate languages: raw-attachment:D4_3.pdf
     95 * D5.1 Untrusted CerCo Prototype: raw-attachment:D5_1.pdf
    8196 * D6.1 Project website and software repository: raw-attachment:D6_1.pdf
    8297 * D6.2 Plan for the use and dissemination of the foreground: raw-attachment:D6_2.pdf
     98 * D3.4 Front-end correctness proof: raw-attachment:D3_4.pdf
     99 * D4.4 Back-end correctness proof: raw-attachment:D4_4.pdf
     100 * D5.2 Trust CerCo Prototype: raw-attachment:D5_2.pdf
     101 * D5.3 Case study: raw-attachment:D5_3.pdf
     102 * D6.2 CerCo workshop and pubblication planning: raw-attachment:D6.2-supplement.pdf
     103 * D6.3 Final Report on User Valuation: raw-attachment:D6_3.pdf
     104 * D6.4 and D6.5 Organization of an Event Targeted to Potential Industrial Stakeholders and Organization of an Event Targeted to Scientific Community: raw-attachment:D6_4_D6_5.pdf
     105 * D6.6 Package for Linux Distribution and Live CD: raw-attachment:D6_6.pdf
    84107=== Members ===