- CORDIS - PROJECTS 16/12/2009
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 comprises 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.
Start date: 2010-02-01
End date: 2013-01-31
Duration: 36 months
Project Reference: 243881
Project cost: 1.52 million euro
Project Funding: 1.16 million euro
Subprogramme Area: ICT-2007.8.0 FET Open
Contract type: Collaborative project (generic)
Coordinatore: ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA - ITALY - SACERDOTI COEN, CLAUDIO
- UNIVERSITE PARIS DIDEROT - PARIS 7 - FRANCE
- THE UNIVERSITY OF EDINBURGH - UNITED KINGDOM
|Quadro di finanziamento||
|Area di interesse||