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

doi:10.1007/978-3-319-12466-7_1

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 proceeding › Conference contribution

19 Citations (Scopus)

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.

Original language	English
Title of host publication	Foundational and Practical Aspects of Resource Analysis. FOPARA 2013
Editors	Ugo Dal Lago, Ricardo Peña
Publisher	Springer
Pages	1-18
Number of pages	18
ISBN (Electronic)	9783319124667
ISBN (Print)	9783319124650
DOIs	https://doi.org/10.1007/978-3-319-12466-7_1
Publication status	Published - 2014
Event	3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013 - Bertinoro, Italy Duration: 29 Aug 2013 → 31 Aug 2013

Publication series

Name	Lecture Notes in Computer Science
Volume	8552
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013
Abbreviated title	FOPARA 2013
Country/Territory	Italy
City	Bertinoro
Period	29/08/13 → 31/08/13

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-12466-7_1

Cite this

Amadio, R. M., Ayache, N., Bobot, F., Boender, J. P., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D. P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C. S., Stark, I., & Tranquilli, P. (2014). Certified Complexity (CerCo). In U. D. Lago, & R. Peña (Eds.), Foundational and Practical Aspects of Resource Analysis. FOPARA 2013 (pp. 1-18). (Lecture Notes in Computer Science; Vol. 8552). Springer. https://doi.org/10.1007/978-3-319-12466-7_1

@inproceedings{b824778fc34a4432bfb601f002fbcfe6,

title = "Certified Complexity (CerCo)",

abstract = "We provide an overview of the FET-Open Project CerCo ({\textquoteleft}Certified Complexity{\textquoteright}). 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.",

author = "Amadio, {Roberto M.} and Nicolas Ayache and Francois Bobot and Boender, {Jaap P.} and Brian Campbell and Ilias Garnier and Antoine Madet and James McKinna and Mulligan, {Dominic P.} and Mauro Piccolo and Randy Pollack and Yann R{\'e}gis-Gianas and Coen, {Claudio Sacerdoti} and Ian Stark and Paolo Tranquilli",

year = "2014",

doi = "10.1007/978-3-319-12466-7_1",

language = "English",

isbn = "9783319124650",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "1--18",

editor = "Lago, {Ugo Dal} and Ricardo Pe{\~n}a",

booktitle = "Foundational and Practical Aspects of Resource Analysis. FOPARA 2013",

note = "3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013, FOPARA 2013 ; Conference date: 29-08-2013 Through 31-08-2013",

}

Amadio, RM, Ayache, N, Bobot, F, Boender, JP, Campbell, B, Garnier, I, Madet, A, McKinna, J, Mulligan, DP, Piccolo, M, Pollack, R, Régis-Gianas, Y, Coen, CS, Stark, I & Tranquilli, P 2014, Certified Complexity (CerCo). in UD Lago & R Peña (eds), Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science, vol. 8552, Springer, pp. 1-18, 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013, Bertinoro, Italy, 29/08/13. https://doi.org/10.1007/978-3-319-12466-7_1

TY - GEN

T1 - Certified Complexity (CerCo)

AU - Amadio, Roberto M.

AU - Ayache, Nicolas

AU - Bobot, Francois

AU - Boender, Jaap P.

AU - Campbell, Brian

AU - Garnier, Ilias

AU - Madet, Antoine

AU - McKinna, James

AU - Mulligan, Dominic P.

AU - Piccolo, Mauro

AU - Pollack, Randy

AU - Régis-Gianas, Yann

AU - Coen, Claudio Sacerdoti

AU - Stark, Ian

AU - Tranquilli, Paolo

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84909639253&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-12466-7_1

DO - 10.1007/978-3-319-12466-7_1

M3 - Conference contribution

AN - SCOPUS:84909639253

SN - 9783319124650

T3 - Lecture Notes in Computer Science

SP - 1

EP - 18

BT - Foundational and Practical Aspects of Resource Analysis. FOPARA 2013

A2 - Lago, Ugo Dal

A2 - Peña, Ricardo

PB - Springer

T2 - 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis 2013

Y2 - 29 August 2013 through 31 August 2013

ER -

Certified Complexity (CerCo)

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this