CERTIFIED COMPLEXITY
(CerCo)
Date du début: 1 févr. 2010,
Date de fin: 31 mars 2013
PROJET
TERMINÉ
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.
Accédez au prémier réseau pour la cooperation européenne
Se connecter
ou
Créer un compte
Pour accéder à toutes les informations disponibles
Coordinateur
ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA
€ 429 565,00- Claudio Sacerdoti Coen
- Via Mura Anteo Zamboni 7 40126 BOLOGNA (Italy)
2 Participants partenaires
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)