Abstract
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. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Campbell, B. (2012). An executable semantics for CompCert C. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 60–75). https://doi.org/10.1007/978-3-642-35308-6_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
