CerCo
CERTIFIED COMPLEXITY
| Coordinatore | ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA
Organization address
address: Via Mura Anteo Zamboni 7 contact info |
| Nazionalità Coordinatore | Italy [IT] |
| Totale costo | 1˙528˙094 € |
| EC contributo | 1˙164˙533 € |
| Programma | FP7-ICT
Specific Programme "Cooperation": Information and communication technologies |
| Code Call | FP7-ICT-2009-C |
| Funding Scheme | CP |
| Anno di inizio | 2010 |
| Periodo (anno-mese-giorno) | 2010-02-01 - 2013-03-31 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA
Organization address
address: Via Mura Anteo Zamboni 7 contact info |
IT (BOLOGNA) | coordinator | 0.00 |
| 2 |
THE UNIVERSITY OF EDINBURGH
Organization address
address: OLD COLLEGE, SOUTH BRIDGE contact info |
UK (EDINBURGH) | participant | 0.00 |
| 3 |
UNIVERSITE PARIS DIDEROT - PARIS 7
Organization address
address: RUE THOMAS MANN contact info |
FR (PARIS) | participant | 0.00 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
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.nThe compiler will be open source, and all proofs will be public domain.