Personal tools
You are here: Home Events Ian Stark: CerCo: Certified Complexity

Ian Stark: CerCo: Certified Complexity

When Jul 24, 2012
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal

I'll describe CerCo, a European research project to build a verified C compiler that provides cycle-precise execution costs for an embedded microcontroller.  It's a collaboration between groups in Bologna, Edinburgh and Paris: Edinburgh participants are Randy Pollack, Brian Campbell, Ilias Garnier, James McKinna and myself.

The project result is to be a compiler that takes C source code and generates both a binary microcontroller executable and annotations on the source that indicate the runtime cost of each piece of code.  This will be formally verified, meaning that there is a machine-checked mathematical proof of two properties: the executable correctly implements the source program; and the cost annotations exactly describe the runtime behaviour of that executable. These certified annotations provide a reliable infrastructure for programmers to reason about source code while ensuring precise performance of the target executable.

Document Actions