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

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

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

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
Subtitle of host publication	Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013
Publisher	Springer International Publishing
Pages	1-18
Number of pages	18
ISBN (Electronic)	978-3-319-12466-7
ISBN (Print)	978-3-319-12465-0
DOIs	https://doi.org/10.1007/978-3-319-12466-7_1
Publication status	Published - 2014

Publication series

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

Access to Document

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

fopara13-author-finalAccepted author manuscript, 295 KB

http://dx.doi.org/10.1007/978-3-319-12466-7_1

1 Finished

CerCo: Certified Complexity
Stark, I.
EU government bodies
1/02/10 → 31/03/13
Project: Research

Brian Campbell
- Brian.Campbelled.acuk
- School of Informatics - Senior Researcher
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active (Research Assistant)
Ian Stark
- Ian.Starked.acuk
- School of Informatics - Senior Lecturer
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active

Cite this

Amadio, R., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D., Piccolo, M., Pollack, R., Régis-Giannas, Y., Sacerdoti Coen, C., Stark, I., & Tranquilli, P. (2014). Certified Complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013 (pp. 1-18). (Lecture Notes in Computer Science; Vol. 8552). Springer International Publishing. https://doi.org/10.1007/978-3-319-12466-7_1

Amadio, Roberto ; Ayache, Nicolas ; Bobot, Francois ; Boender, Jaap ; Campbell, Brian ; Garnier, Ilias ; Madet, Antoine ; McKinna, James ; Mulligan, Dominic ; Piccolo, Mauro ; Pollack, Robert ; Régis-Giannas, Yann ; Sacerdoti Coen, Claudio ; Stark, Ian ; Tranquilli, Paolo. / Certified Complexity (CerCo). Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Springer International Publishing, 2014. pp. 1-18 (Lecture Notes in Computer Science).

@inproceedings{83417580f556481da81de0a1df149849,

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 = "Roberto Amadio and Nicolas Ayache and Francois Bobot and Jaap Boender and Brian Campbell and Ilias Garnier and Antoine Madet and James McKinna and Dominic Mulligan and Mauro Piccolo and Robert Pollack and Yann R{\'e}gis-Giannas and {Sacerdoti Coen}, Claudio and Ian Stark and Paolo Tranquilli",

year = "2014",

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

language = "English",

isbn = "978-3-319-12465-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "1--18",

booktitle = "Foundational and Practical Aspects of Resource Analysis",

}

Amadio, R, Ayache, N, Bobot, F, Boender, J, Campbell, B, Garnier, I, Madet, A, McKinna, J, Mulligan, D, Piccolo, M, Pollack, R, Régis-Giannas, Y, Sacerdoti Coen, C, Stark, I & Tranquilli, P 2014, Certified Complexity (CerCo). in Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Lecture Notes in Computer Science, vol. 8552, Springer International Publishing, pp. 1-18. https://doi.org/10.1007/978-3-319-12466-7_1

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

Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Springer International Publishing, 2014. p. 1-18 (Lecture Notes in Computer Science; Vol. 8552).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Certified Complexity (CerCo)

AU - Amadio, Roberto

AU - Ayache, Nicolas

AU - Bobot, Francois

AU - Boender, Jaap

AU - Campbell, Brian

AU - Garnier, Ilias

AU - Madet, Antoine

AU - McKinna, James

AU - Mulligan, Dominic

AU - Piccolo, Mauro

AU - Pollack, Robert

AU - Régis-Giannas, Yann

AU - Sacerdoti Coen, Claudio

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.

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

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

M3 - Conference contribution

SN - 978-3-319-12465-0

T3 - Lecture Notes in Computer Science

SP - 1

EP - 18

BT - Foundational and Practical Aspects of Resource Analysis

PB - Springer International Publishing

ER -

Amadio R, Ayache N, Bobot F, Boender J, Campbell B, Garnier I et al. Certified Complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Springer International Publishing. 2014. p. 1-18. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-12466-7_1

Certified Complexity (CerCo)

Abstract

Publication series

Access to Document

Fingerprint

Projects

CerCo: Certified Complexity

Profiles

Brian Campbell

Ian Stark

Cite this