CerCo: Certifying Costs in a Certified Compiler
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.
|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)|
|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)|
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 firstname.lastname@example.org.