Certified Complexity (CerCo)

Roberto Amadio, Nicolas Ayache, Francois Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic Mulligan, Mauro Piccolo, Robert Pollack, Yann Régis-Giannas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We provide an overview of the FET-Open Project CerCo (‘Certified Complexity’). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base. The core component is a C compiler, verified in Matita, that produces an instrumented copy of the source code in addition to generating object code. This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.
Original languageEnglish
Title of host publicationFoundational and Practical Aspects of Resource Analysis
Subtitle of host publicationRevised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013
PublisherSpringer International Publishing
Number of pages18
ISBN (Electronic)978-3-319-12466-7
ISBN (Print)978-3-319-12465-0
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Certified Complexity (CerCo)'. Together they form a unique fingerprint.

Cite this