CerCo --- Certified Complexity

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

• Dominic Mulligan (Bologna)
• Thursday 31 May 2012, 11:00-12:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.