CerCo

CERTIFIED COMPLEXITY

Coordinatore	ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA    more  Organization address address: Via Mura Anteo Zamboni 7 city: BOLOGNA postcode: 40126 contact info Titolo: Dr. Nome: Claudio Cognome: Sacerdoti Coen Email: send email Telefono: 390512000000 Fax: 390512000000
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

#	participant	country	role	EC contrib. [€]
1	ALMA MATER STUDIORUM-UNIVERSITA DI BOLOGNA  Organization address address: Via Mura Anteo Zamboni 7 city: BOLOGNA postcode: 40126 contact info Titolo: Dr. Nome: Claudio Cognome: Sacerdoti Coen Email: send email Telefono: 390512000000 Fax: 390512000000	IT (BOLOGNA)	coordinator	0.00
2	THE UNIVERSITY OF EDINBURGH  Organization address address: OLD COLLEGE, SOUTH BRIDGE city: EDINBURGH postcode: EH8 9YL contact info Titolo: Mr. Nome: Gordon Cognome: Marshall Email: send email Telefono: +44 131 6514386 Fax: +44 131 6509031	UK (EDINBURGH)	participant	0.00
3	UNIVERSITE PARIS DIDEROT - PARIS 7  Organization address address: RUE THOMAS MANN city: PARIS postcode: 75205 contact info Titolo: Ms. Nome: Anne Cognome: BONVALET Email: send email Telefono: +331 57275559 Fax: +331 57275547	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.