Unibo Team Leader: Dott. Claudio Sacerdoti Coen, Dip. di Scienze dell'Informazione
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.
Coordinator
ALMA MATER STUDIORUM-UNIVERSITA' DI BOLOGNA
- Dip. di Scienze dell'Informazione
- Resp. Scientifico: Dott. Claudio Sacerdoti Coen
Other participants
UNIVERSITE PARIS DIDEROT - PARIS 7 (France)
THE UNIVERSITY OF EDINBURGH (UK)
Start date 01/02/2010
End date 31/01/2013
Duration 36 months
Project cost 1.523.743 EURO
Project Funding 1.164.533 EURO
Subprogramme Area ICT-2007.8.0: FET Open
Contract type Collaborative project