Personal tools
You are here: Home Events Lab Lunch: Dr Brian Campbell

Lab Lunch: Dr Brian Campbell

An executable semantics for CompCert

What
When Sep 06, 2011
from 01:00 PM to 02:00 PM
Where Informatics Forum MF2
Contact Name
Add event to calendar vCal
iCal

CompCert is a C compiler developed by Leroy et al, the majority of which is formalised and verified in the Coq proof assistant. The correctness theorem is defined in terms of a semantics for the "CompCert C" language, but how can we gain faith in those semantics? We explore one approach: building an equivalent executable semantics that we can check test suites of code against.

Document Actions