CERTIFIED COMPLEXITY
(CerCo)
Start date: Feb 1, 2010,
End date: Mar 31, 2013
PROJECT
FINISHED
The project aims to the construction of a formally verified complexity preserving compiler from a large subset of C to some typical microcontroller assembly, of the kind traditionally used in embedded systems. The work comprise the definition of cost models for the input and target languages, and the machine-checked proof of preservation of complexity (concrete, not asymptotic) along compilation. The compiler will also return tight and certified cost annotations for the source program, providing a reliable infrastructure to draw temporal assertions on the executable code while reasoning on the source.The compiler will be open source, and all proofs will be public domain.
Get Access to the 1st Network for European Cooperation
Log In
or
Create an account
to see this content
Coordinator
ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA
€ 429 565,00- Claudio Sacerdoti Coen
- Via Mura Anteo Zamboni 7 40126 BOLOGNA (Italy)
2 Partners Participants
UNIVERSITE PARIS DIDEROT - PARIS 7
€ 314 457,00- Anne BONVALET
- RUE THOMAS MANN 75205 PARIS (France)
THE UNIVERSITY OF EDINBURGH
€ 420 511,00- Gordon Marshall
- OLD COLLEGE, SOUTH BRIDGE EH8 9YL EDINBURGH (United Kingdom)