An Executable Semantics for CompCert C

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationCertified Programs and Proofs
Subtitle of host publicationSecond International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings
EditorsChris Hawblitzel, Dale Miller
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-35308-6
ISBN (Print)978-3-642-35307-9
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint Dive into the research topics of 'An Executable Semantics for CompCert C'. Together they form a unique fingerprint.

Cite this