Version 30 (modified by mulligan, 6 years ago) (diff) |
---|
Certified Complexity (CerCo)
CerCo (Certified Complexity) is a European research project in the 7th Research Framework Programme (FP7) of the European Commission (project number 243381). The project is situated in the FP7 theme Information & Communication Technologies (ICT) in the topic Future and Emerging Technologies (FET Open). The project has started February 1st, 2010, and will have a duration of 3 years.
The 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.
Related work
A collection of links to work similar to CerCo can be found here.
Potential outlets for publicaton
A list of potential workshops, conferences and journals suitable for CerCo publications can be found here.
Publications
Publications that fall under the aegis of the CerCo project:
- On the correctness of an assembler for the MCS-51 microprocessor. Dominic P. Mulligan and Claudio Sacerdoti Coen. Submitted to CPP 2011. Matita formalisation here.
- Semantics for simple type theory in nominal sets. Murdoch J. Gabbay and Dominic P. Mulligan. Submitted to LFMTP 2011.
- An executable formalisation of the MCS-51 microprocessor in Matita. Dominic P. Mulligan and Claudio Sacerdoti Coen. Submitted to FMCAD 2011.
- Certifying cost annotations in compilers. Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas and Ronan Saillard. Technical Report, Université Paris Diderot (Paris 7).
Learn More
- Concept and Objectives, progress beyond state-of-the-art, S/T methodology and work plan
- Implementation
- Potential impact
Deliverables
- D2.1 Compiler design and intermediate languages: raw-attachment:D2_1.pdf
- D2.2 Prototype implementation: raw-attachment:D2_2.pdf
- D3.1 Executable formal semantics of C: raw-attachment:D3_1.pdf
- D4.1 Executable formal semantics of machine code: raw-attachment:D4_1.pdf raw-attachment:D4_1_Code.tar.gz
- D6.1 Project website and software repository: raw-attachment:D6_1.pdf
- D6.2 Plan for the use and dissemination of the foreground: raw-attachment:D6_2.pdf
Members
University of Bologna (coordinator)
- Dr. Claudio Sacerdoti Coen (Project Leader)
- Prof Andrea Asperti
- Dr. Enrico Tassi (invited researcher, INRIA)
- Dr. Dominic Mulligan (Post-Doc)
- Dr. Jaap Boender (Post-Doc)
- Dr. Wilmer Ricciotti (PhD student)
- Mr. Matthias Puech (PhD student)
- Dr. Ian Stark (Site Leader)
- Dr. Randy Pollack
- Dr. Brian Campbell
- Prof. Roberto Amadio (Site Leader)
- Dr. Yann Régis-Gianas
- Dr. Nicolas Ayache (Post-Doc)
- Mr. Ronan Saillard
- Mr. Kayvan Memarian
Attachments (44)
- D6_1.pdf (308.4 KB) - added by sacerdot 8 years ago.
- D2_1.pdf (831.2 KB) - added by mulligan 7 years ago.
- D2_2.pdf (446.9 KB) - added by mulligan 7 years ago.
- D3_1.pdf (478.3 KB) - added by mulligan 7 years ago.
- D4_1.pdf (487.1 KB) - added by mulligan 7 years ago.
- D6_2.pdf (325.3 KB) - added by mulligan 7 years ago.
- D4_1_Code.tar.gz (56.1 KB) - added by mulligan 7 years ago.
-
D5.1-5.3.tar.gz
(629.8 KB) -
added by mulligan 6 years ago.
Deliverable for D5.1-5.3
-
D3-2.pdf
(392.3 KB) -
added by mulligan 6 years ago.
Deliverable for D3.2
-
D3-3.pdf
(24.2 KB) -
added by mulligan 6 years ago.
Deliverable for D3.3
-
src20111020.tgz
(869.2 KB) -
added by mulligan 6 years ago.
Matita snapshot for typechecking recent deliverables
-
D5.1-5.3.pdf
(1.5 MB) -
added by mulligan 6 years ago.
Report for D5.1-5.3
-
Matita-18-06-2012.tar.gz
(25.9 MB) -
added by mulligan 6 years ago.
Matita snapshot for typechecking CPP submissions
-
CPP2012.tar.gz
(2.6 MB) -
added by mulligan 6 years ago.
Latest snapshot of CerCo? proof.
-
cost-plug-in-0.2.tgz
(95.0 KB) -
added by regisgia 5 years ago.
Frama-C (Nitrogen) Cost plugin
-
acc_0.2-1_amd64.deb
(672.7 KB) -
added by sacerdot 5 years ago.
Untrusted CerCo? Compiler, Debian package
-
acc-trusted_0.2-1_amd64.deb
(1.1 MB) -
added by sacerdot 5 years ago.
Trusted CerCo? Compiler, Debian package
-
frama-c-cost-plugin_0.2-1_amd64.deb
(855.8 KB) -
added by sacerdot 5 years ago.
CerCo?'s Frama-C Cost Plugin, Debian package
-
libwhy-coq_2.31+cerco-1_all.deb
(339.9 KB) -
added by sacerdot 5 years ago.
Part of the why suite, modified for CerCo?. Debian package
-
why_2.31+cerco-1_amd64.deb
(7.7 MB) -
added by sacerdot 5 years ago.
Part of the why suite, modified for CerCo?. Debian package
-
why-examples_2.31+cerco-1_all.deb
(332.3 KB) -
added by sacerdot 5 years ago.
Part of the why suite, modified for CerCo?. Debian package
-
why3_0.73+cerco-1_amd64.deb
(22.2 MB) -
added by sacerdot 5 years ago.
Why3 suite, Debian package.
-
matita_0.99.2-1_amd64.deb
(4.3 MB) -
added by sacerdot 5 years ago.
Matita 0.99.2, compatible with the CerCo? sources. Debian package.
-
cvc3_2.4.1-1_amd64.deb
(6.5 MB) -
added by sacerdot 5 years ago.
The CVC3 theorem prover, Debian package
- cost-plug-in_0.2.orig.tar.gz (80.2 KB) - added by sacerdot 5 years ago.
- certification_20130430.tgz (982.9 KB) - added by sacerdot 5 years ago.
- acc-trusted_0.2.orig.tar.gz (561.0 KB) - added by sacerdot 5 years ago.
- acc_0.2.orig.tar.gz (1019.0 KB) - added by sacerdot 5 years ago.
- D3_4.pdf (692.2 KB) - added by sacerdot 5 years ago.
- D4_4.pdf (885.0 KB) - added by sacerdot 5 years ago.
- D5_2.pdf (362.2 KB) - added by sacerdot 5 years ago.
- D5_3.pdf (1.9 MB) - added by sacerdot 5 years ago.
- D6_3.pdf (504.1 KB) - added by sacerdot 5 years ago.
- D6_4_D6_5.pdf (261.8 KB) - added by sacerdot 5 years ago.
- D6_6.pdf (279.9 KB) - added by sacerdot 5 years ago.
- D6.2-supplement.pdf (284.2 KB) - added by sacerdot 5 years ago.
- D5-1-software.tgz (470.6 KB) - added by sacerdot 5 years ago.
- D5-1-cost_plug_in.tgz (45 bytes) - added by sacerdot 5 years ago.
- D5-1.pdf (708.6 KB) - added by sacerdot 5 years ago.
-
D4-3.pdf
(372.4 KB) -
added by sacerdot 5 years ago.
Deliverable for D4.3
-
D4-2.pdf
(371.1 KB) -
added by sacerdot 5 years ago.
Deliverable for D4.2
- D2-1-addendum.pdf (396.7 KB) - added by sacerdot 5 years ago.
- cpp-2011.pdf (331.5 KB) - added by sacerdot 5 years ago.
- CPP2013.tar.gz (62.4 KB) - added by sacerdot 5 years ago.