Changes between Version 45 and Version 46 of WikiStart


Ignore:
Timestamp:
May 1, 2013, 1:25:08 AM (4 years ago)
Author:
sacerdot
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v45 v46  
    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.
    66
    7 == Debian Packages for the CerCo Software ==
     7== !CerCo's Live CD ==
    88
    9 We provide Debian packages for all the software developed in CerCo and its dependencies.
     9Try out !CerCo's Live CD: [http://cerco.cs.unibo.it/livecd/binary.hybrid.iso]
     10You can boot your machine with the Live CD or you can emulate it using a virtual machine
     11(virtualbox reccommended). Once logged in, you can try the Frama-C Cost Annotating Compiler
     12by running  "cerco -ide filename.c" or you can browse the certification of the !CerCo's compiler
     13running "matita" and exploring the source code in the cerco/src directory.
     14
     15== Debian Packages for the !CerCo Software ==
     16
     17Tired of the Live CD? We provide Debian packages for all the software developed in !CerCo and its dependencies.
    1018
    1119 * raw-attachment:acc_0.2-1_amd64.deb
    12    CerCo's Cost Annotating Compiler
     20   !CerCo's Cost Annotating Compiler
    1321 * raw-attachment:acc-trusted_0.2-1_amd64.deb
    14    Trusted CerCo's Cost Annotating Compiler
     22   Trusted !CerCo's Cost Annotating Compiler
    1523 * raw-attachment:frama-c-cost-plugin_0.2-1_amd64.deb
    16    CerCo's Frama-C Cost Plugin
     24   !CerCo's Frama-C Cost Plugin
    1725 * raw-attachment:why_2.31+cerco-1_amd64.deb, raw-attachment:libwhy-coq_2.31+cerco-1_all.deb, raw-attachment:why-examples_2.31+cerco-1_all.deb
    18    A version of the why suite compatible with CerCo's Frama-C Cost Plugin
     26   A version of the why suite compatible with !CerCo's Frama-C Cost Plugin
    1927 * raw-attachment:why3_0.73+cerco-1_amd64.deb
    20    A version of the why3 suite compatible with CerCo's Frama-C Cost Plugin. It must be installed together with why.
     28   A version of the why3 suite compatible with !CerCo's Frama-C Cost Plugin. It must be installed together with why.
    2129 * raw-attachment:cvc3_2.4.1-1_amd64.deb
    22    The automated theorem prover cvc3, able to close most proof obligations generated by the CerCo's Frama-C Cost Plugin.
     30   The automated theorem prover cvc3, able to close most proof obligations generated by the !CerCo's Frama-C Cost Plugin.
    2331 * raw-attachment:matita_0.99.2-1_amd64.deb
    24    A version of Matita that can process the CerCo's certification of the Trusted CerCo's Cost Annotating Compiler
     32   A version of Matita that can process the !CerCo's certification of the Trusted !CerCo's Cost Annotating Compiler
    2533
    2634== !CerCo workshops ==