University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > CerCo --- Certified Complexity

CerCo --- Certified Complexity

Add to your list(s) Download to your calendar using vCal

  • UserDominic Mulligan (Bologna)
  • ClockThursday 31 May 2012, 11:00-12:00
  • HouseFW26.

If you have a question about this talk, please contact Peter Sewell.

NB: Unusual day/time

CerCo is a joint verified compiler project between the universities of Bologna, Edinburgh and Paris VII (Diderot). Similar in spirit to Leroy’s CompCert project, we aim to build a verified compiler for a large subset of C. However, unlike CompCert, we also aim to lift a certified and tight concrete cost model, as induced by compilation, back through the compiler to the C source level. This cost model will be reflected as a series of cost annotations on the input C source which may be used by existing automated reasoning tools to derive precise concrete execution time bounds for the input program.

In this talk, I will discuss some of the motivations for the CerCo project, our current progress towards completion, and some details of the (compiler backend, mostly) proofs.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity