![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Dominic Mulligan (Bologna)
Thursday 31 May 2012, 11:00-12:00
CerCo --- Certified Complexity
- 👤 Speaker: Dominic Mulligan (Bologna)
- 📅 Date & Time: Thursday 31 May 2012, 11:00 - 12:00
- 📍 Venue: FW26
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Martin's interesting talks
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.