• Condividi su Facebook

CERCO - Certified complexity

  • 21275
  • CORDIS - PROJECTS 16/12/2009
  • RISULTATO

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

Altri Partecipanti

  • UNIVERSITE PARIS DIDEROT - PARIS 7 - FRANCE
  • THE UNIVERSITY OF EDINBURGH - UNITED KINGDOM
Link
Quadro di finanziamento
  • 7FP-ICT : TECNOLOGIE DELL’INFORMAZIONE E DELLA COMUNICAZIONE: priorità tematica 3 nell'ambito del programma specifico “Cooperazione” recante attuazione del Settimo programma quadro (2007-2013) di attività comunitarie di ricerca, sviluppo tecnologico e dimostrazione
Area di interesse
  • Unione Europea