Version 3 (modified by campbell, 6 years ago) (diff)


CerCo: Certifying Costs in a Certified Compiler

HiPEAC 2013 half-day workshop

The CerCo workshop considers the construction of formally verified compilers for embedded systems that can be used to certify timing bounds at the level of source code.

The workshop has two objectives:

  • To publicise the results of CerCo FP7 project to members of the relevant industrial and academic research communities.
  • To stimulate discussion between the industrial and academic participants about future work building on the current state of the art.

The CerCo project links a low level cycle precise execution time analysis with an innovative source code labelling approach that presents the results of the timing analysis in annotated source code. This allows high level reasoning about the execution time of compiled programs. We combine this with formal verification of the compilation process to obtain a high level of assurance about the correctness and performance of the compiled code.

The draft programme for the workshop consists of:

  • Short talks by CerCo partners presenting the project and its results.
    • Project overview: a trustworthy framework for cost analysis of embedded code.
    • The labelling approach to cost analysis: a modular way to prove correctness; and methods to reason about the cost annotations and their application
    • The verified CerCo compiler: what makes a certified compiler trustworthy.
    • Dependent labels: managing refined cost information for richer architectures.
    • Future directions: the latest very-low-power embedded processors; other runtime costs; further languages.
  • Short presentations by some of the invited participants on the state of the art in static analysis of execution costs for embedded systems and future challenges.


Participation in the workshop is open. It is taking place as part of the HiPEAC 2013 conference in Berlin, January 21‐23, 2013. All attendees should register for the main conference.

Organizers and their affiliations

You can contact the organisers at cerco-workshop@….

Attachments (1)

Download all attachments as: .zip