BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CerCo --- Certified Complexity - Dominic Mulligan (Bologna)
DTSTART:20120531T100000Z
DTEND:20120531T110000Z
UID:TALK38348@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:CerCo is a joint verified compiler project between the univers
 ities of Bologna\, Edinburgh and Paris VII (Diderot).  Similar in spirit t
 o Leroy's CompCert project\, we aim to build a verified compiler for a lar
 ge subset of C.  However\, unlike CompCert\, we also aim to lift a certifi
 ed and tight concrete cost model\, as induced by compilation\, back throug
 h the compiler to the C source level.  This cost model will be reflected a
 s a series of cost annotations on the input C source which may be used by 
 existing automated reasoning tools to derive precise concrete execution ti
 me bounds for the input program.\n\nIn this talk\, I will discuss some of 
 the motivations for the CerCo project\, our current progress towards compl
 etion\, and some details of the (compiler backend\, mostly) proofs.
LOCATION:FW26
END:VEVENT
END:VCALENDAR