Certified Complexity (CerCo)

Conference paper

Amadio, R., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D., Piccolo, M., Pollack, R., Régis-Gianas, Y., Sacerdoti Coen, C., Stark, I. and Tranquilli, P. 2014. Certified Complexity (CerCo). Third International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA 2013). Bertinoro, Italy 29 - 31 Aug 2013 https://doi.org/10.1007/978-3-319-12466-7_1
TypeConference paper
TitleCertified Complexity (CerCo)
AuthorsAmadio, R., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D., Piccolo, M., Pollack, R., Régis-Gianas, Y., Sacerdoti Coen, C., Stark, I. and Tranquilli, P.
Abstract

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.

Research GroupFoundations of Computing group
ConferenceThird International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA 2013)
ISSN0302-9743
ISBN
Hardcover9783319124650
Publication dates
Print2014
Publication process dates
Deposited11 May 2015
Output statusPublished
Copyright Statement

Access to full text restricted pending copyright check.

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-12466-7_1
LanguageEnglish
Book titleFoundational and Practical Aspects of Resource Analysis: Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers
Permalink -

https://repository.mdx.ac.uk/item/85450

Log in to edit

Restricted files

Publisher's version

  • 19
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as