= Certified Complexity (!CerCo) =

!CerCo (Certified Complexity) is a European research project in the [http://cordis.europa.eu/fp7/home_en.html 7th Research Framework Programme] (FP7) of the [http://ec.europa.eu/index_en.htm European Commission] (project number 243381). The project is situated in the FP7 theme [http://cordis.europa.eu/fp7/ict/ssai/home_en.html 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.

== Software ==

=== !CerCo's Live CD ===

Try out !CerCo's Live CD: [http://cerco.cs.unibo.it/livecd/binary.hybrid.iso]
You can boot your machine with the Live CD or you can emulate it using a virtual machine
(virtualbox reccommended). Once logged in, you can try the Frama-C Cost Annotating Compiler
by running  "cerco -ide filename.c" or you can browse the certification of the !CerCo compiler
by running "matita" and exploring the source code in the cerco/src directory.

=== Debian Packages for the !CerCo Software ===

Tired of the Live CD? We provide Debian packages for all the software developed in !CerCo and its dependencies.

 * raw-attachment:acc_0.2-1_amd64.deb
   !CerCo Cost Annotating Compiler
 * raw-attachment:acc-trusted_0.2-1_amd64.deb
   Trusted !CerCo Cost Annotating Compiler
 * raw-attachment:frama-c-cost-plugin_0.2-1_amd64.deb
   !CerCo's Frama-C Cost Plugin
 * 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
   A version of the why suite compatible with !CerCo's Frama-C Cost Plugin
 * raw-attachment:why3_0.73+cerco-1_amd64.deb
   A version of the why3 suite compatible with !CerCo's Frama-C Cost Plugin. It must be installed together with why.
 * raw-attachment:cvc3_2.4.1-1_amd64.deb
   The automated theorem prover cvc3, able to close most proof obligations generated by the !CerCo's Frama-C Cost Plugin.
 * raw-attachment:matita_0.99.2-1_amd64.deb
   A version of Matita that can process the !CerCo certification of the Trusted !CerCo Cost Annotating Compiler


=== Source code ===

Source code is provided as well.

 * raw-attachment:acc_0.2.orig.tar.gz !CerCo Cost Annotating Compiler
 * raw-attachment:acc-trusted_0.2.orig.tar.gz Trusted !CerCo Cost Annotating Compiler
 * raw-attachment:certification_20130430.tgz Matita source code of the formal correctness proof
 * raw-attachment:cost-plug-in_0.2.orig.tar.gz !CerCo's Frama-C Cost Plugin

== !CerCo workshops ==

We held two workshops in 2013 featuring results from the !CerCo project:

 * [wiki:HiPEAC13 The CerCo workshop] at HiPEAC'13, Wednesday 23rd January in the afternoon.
 * [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.

=== CPP 2012 submissions ===

Code for the two CerCo CPP 2012 submissions can be found attached to the bottom of this page in the file "CPP2012.tar.gz".  A snapshot of a recent version of Matita for typechecking these submissions can also be found attached in the file "Matita-18-06-2012.tar.gz".  To build Matita, extract the files, change to the target directory, type ./configure and then make world.  An optimised set of Matita binaries (matita.opt) will be built in the "matita" subdirectory.

=== Related work ===

A collection of links to work similar to !CerCo can be found [wiki:RelatedWork here].

=== Potential outlets for publicaton ===

A list of potential workshops, conferences and journals suitable for !CerCo publications can be found [wiki:PublicationVenues 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 [wiki:AssemblerFormalisation 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.
  * [http://hal.archives-ouvertes.fr/hal-00524715/fr/ Certifying cost annotations in compilers].  Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas and Ronan Saillard.  Technical Report, Université Paris Diderot (Paris 7).
  * [http://homepages.inf.ed.ac.uk/rpollack/export/PollackSatoRicciottiJAR.pdf A Canonical Locally Named Representation of Binding], R. Pollack, M. Sato and W. Ricciotti, Journal of Automated Reasoning, 
  * [http://arxiv.org/abs/1110.2350 Certifying and reasoning on cost annotations of functional programs], R.M. Amadio, Y. Regis‐Gianas, In proceedings of Foundations and Practical Aspects of Resource Analysis (FOPARA 2011), LNCS, 71277:72‐89
  * [http://arxiv.org/abs/1102.4971 An Elementary Affine λ‐Calculus with Multithreading and Side Effects], A. Madet, R.M. Amadio., In Proceedings Typed Lambda Calculi and Applications (TLCA 2011), Springer LNCS 6690:138‐152, 2011
  * Certified Complexity, R. Amadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis‐Gianas, C. Sacerdoti Coen, I. Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11), 175‐177
  * [http://matita.cs.unibo.it/PAPERS/system_description2011.pdf The Matita Interactive Theorem Prover], A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi, In Automated Deduction – CADE‐23, LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978‐3‐642‐22437‐9, Pages 64‐69, Volume 6803, Year 2011
  * [http://hal.inria.fr/hal-00702665/ Certifying and Reasoning on Cost Annotations in C Programs], N. Ayache, R.M. Amadio, Y. Régis‐Gianas, in Proc. FMICS, Springer LNCS 7437: 32‐46, 2012
  * [http://www.cs.unibo.it/~asperti/PAPERS/rating.pdf Rating Disambiguation Errors], A. Asperti, W. Ricciotti, In Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP 2012), LNCS, Volume 7679, Pages 240‐‐255, Springer, 2012
  * Certifying and reasoning on cost annotations of functional programs, R.M. Amadio, Y. Régis‐Gianas, in Higher‐order and Symbolic Computation, to appear, 2012
  * [http://proval.lri.fr/publications/bobot12icfem.pdf Separation Predicates: A Taste of Separation Logic in First‐Order Logic], F. Bobot, J.‐C. Filliatre, in Proc. IFCEM, Springer LNCS 7635:167‐181, 2012
  * [http://www.cs.unibo.it/~asperti/PAPERS/matitaweb.pdf A Web Interface for Matita], A. Asperti, W. Ricciotti, In Proceedings of the Conference on Intelligent Computer Mathematics (CICM 2012), LNAI, Volume 7362/2012, Pages 417‐421
  * [http://arxiv.org/abs/1206.4833 Indexed Realizability for Bounded‐Time Programming with References and Type Fixpoints], A. Brunel, A. Madet, In Proc. APLAS, Springer LNCS 7705:264‐279 , 2012
  * [http://hal.inria.fr/docs/00/73/55/44/PDF/ppdp19-madet.pdf A polynomial time λ‐calculus with multithreading and side effects], A. Madet in Proc. ACM‐PPDP, pages 55‐66, 2012
  * [http://homepages.inf.ed.ac.uk/bcampbe2/compcert/ An executable semantics for CompCert C], B. Campbell, in Proceedings of Certified Proofs and Programs 2012, LNCS 7679:60‐75, 2012
  * On the Correctness of an Optimising Assembler for the Intel MCS‐51 Microprocessor, D. Mulligan, C. Sacerdoti Coen, in Proceedings of Certified Proofs and Programs 2012, LNCS 7679:43‐59, 2012: raw-attachment:cpp-2011.pdf
  * [http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf Indexed Labels for Loop Iteration Dependent Costs], P. Tranquilli, in Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and
Systems (QAPL 2013), Rome, 23rd‐24th March 2013, Electronic Proceedings in Theoretical Computer Science, 2013
=== Learn More ===
 1. Concept and Objectives, progress beyond state-of-the-art, S/T methodology and work plan
   1. [wiki:Proposal1.1 Concept and project objective(s)]
   2. [wiki:Proposal1.2 Progress beyond state of the art]
   3. [wiki:Proposal1.3 S/T methodology and associated work plan]
 2. Implementation
   1. [wiki:Proposal2.1 Management structure and procedures]
   2. [wiki:Proposal2.2 Beneficiaries]
   3. [wiki:Proposal2.3 Consortium as a whole]
   4. [wiki:Proposal2.4 Resources to be committed]
 3. Potential impact
   1. [wiki:Proposal3.1 Strategic impact]
   2. [wiki:Proposal3.2 Plan for the use and dissemination of foreground]

=== Deliverables ===
 * D2.1 Compiler design and intermediate languages: raw-attachment:D2-1-addendum.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
 * D4.2 CIC encoding: Back-end: raw-attachment:D4_2.pdf
 * D4.3 Executable formal semantics of back-end intermediate languages: raw-attachment:D4_3.pdf
 * D5.1 Untrusted CerCo Prototype: raw-attachment:D5_1.pdf
 * 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
 * D3.4 Front-end correctness proof: raw-attachment:D3_4.pdf
 * D4.4 Back-end correctness proof: raw-attachment:D4_4.pdf
 * D5.2 Trust CerCo Prototype: raw-attachment:D5_2.pdf
 * D5.3 Case study: raw-attachment:D5_3.pdf
 * D6.2 CerCo workshop and pubblication planning: raw-attachment:D6.2-supplement.pdf
 * D6.3 Final Report on User Valuation: raw-attachment:D6_3.pdf
 * 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
 * D6.6 Package for Linux Distribution and Live CD: raw-attachment:D6_6.pdf

=== Members ===
[http://www.eng.unibo.it/PortaleEn/default.htm University of Bologna] (coordinator)
 * Dr. [http://www.cs.unibo.it/~sacerdot Claudio Sacerdoti Coen] (Project Leader)
 * Prof [http://www.cs.unibo.it/~asperti Andrea Asperti]
 * Dr. [http://www.msr-inria.inria.fr/~gares Enrico Tassi] (invited researcher, INRIA)
 * Dr. [http://dominic-mulligan.co.uk Dominic Mulligan] (Post-Doc)
 * Dr. Jaap Boender (Post-Doc)
 * Dr. [http://www.cs.unibo.it/~tranquil/ Paolo Tranquilli] (Post-Doc)
 * Dr. [http://www.cs.unibo.it/en/people/phd-students/ricciott.html Wilmer Ricciotti] (PhD student)
 * Mr. [http://www.cs.unibo.it/en/people/phd-students/puech.html Matthias Puech] (PhD student)

[http://www.ed.ac.uk/home University of Edinburgh]
 * Dr. [http://homepages.inf.ed.ac.uk/stark/ Ian Stark] (Site Leader)
 * Dr. [http://homepages.inf.ed.ac.uk/rpollack/ Randy Pollack]
 * Dr. [http://homepages.inf.ed.ac.uk/bcampbe2/ Brian Campbell]
 * Dr. [http://www.inf.ed.ac.uk/people/staff/Ilias_Garnier.html Ilias Garnier]
 * Dr. [http://www.inf.ed.ac.uk/people/staff/James_McKinna.html James McKinna]

[http://www.univ-paris-diderot.fr/ Université Paris Diderot]
 * Prof. [http://www.pps.jussieu.fr/~amadio/ Roberto Amadio] (Site Leader)
 * Dr. [http://www.pps.jussieu.fr/~yrg/  Yann Régis-Gianas]
 * Dr. Nicolas Ayache (Post-Doc)
 * Mr. Ronan Saillard
 * Mr. Kayvan Memarian