wiki:HiPEAC13

CerCo: Certifying Costs in a Certified Compiler

HiPEAC 2013 half-day workshop == HiPEAC logo

Wednesday 23rd January 2013

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.

Programme

14:00-14:30 Certified complexity: a general introduction (Claudio Sacerdoti Coen)
14:30-15:15 Certifying and reasoning on cost annotations of C programs (Yann Régis-Gianas)
15:15-16:00 Dealing with loop optimizations and pipelines (Paolo Tranquilli)
Break
16:30-17:00 Invited talk by Kevin Hammond: Hume: a Functionally-based Domain Specific Language Targeting Real-time Embedded Systems
17:00-17:30 Certifying and reasoning on cost annotations of functional programs (Roberto Amadio)
17:30-18:00 A certified proof based on structured traces (Brian Campbell)

Attendence

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. If you have already registered for the conference, you can indicate that you are attending the workshop by logging into the HiPEAC website and using the Edit Registration Info button on the conference registration page.

Organizers and their affiliations

You can contact the organisers at cerco-workshop@inf.ed.ac.uk.

Last modified 5 years ago Last modified on Jan 21, 2013, 11:22:32 AM

Attachments (1)

Download all attachments as: .zip