Certified Complexity (CerCo)

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

*Corresponding author for this work

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

19 Citations (Scopus)


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. FOPARA 2013
EditorsUgo Dal Lago, Ricardo Peña
Number of pages18
ISBN (Electronic)9783319124667
ISBN (Print)9783319124650
Publication statusPublished - 2014
Event3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013 - Bertinoro, Italy
Duration: 29 Aug 201331 Aug 2013

Publication series

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


Conference3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013
Abbreviated titleFOPARA 2013

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this