An Executable Semantics for CompCert C

Brian Campbell

doi:10.1007/978-3-642-35308-6_8

An Executable Semantics for CompCert C

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

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 language	English
Title of host publication	Certified Programs and Proofs
Subtitle of host publication	Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings
Editors	Chris Hawblitzel, Dale Miller
Publisher	Springer
Pages	60-75
Number of pages	16
ISBN (Electronic)	978-3-642-35308-6
ISBN (Print)	978-3-642-35307-9
DOIs	https://doi.org/10.1007/978-3-642-35308-6_8
Publication status	Published - 2012

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	7679
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-642-35308-6_8

BrianCampbell2012paperAccepted author manuscript, 400 KB

http://dx.doi.org/10.1007/978-3-642-35308-6_8

Cite this

@inproceedings{be8c6a4c31974218b29a97cd9ecb1fcf,

title = "An Executable Semantics for CompCert C",

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 {\textquoteleft}CompCert C{\textquoteright} 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.",

author = "Brian Campbell",

year = "2012",

doi = "10.1007/978-3-642-35308-6_8",

language = "English",

isbn = "978-3-642-35307-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "60--75",

editor = "Chris Hawblitzel and Dale Miller",

booktitle = "Certified Programs and Proofs",

}

An Executable Semantics for CompCert C. / Campbell, Brian.
Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings. ed. / Chris Hawblitzel; Dale Miller. Springer, 2012. p. 60-75 (Lecture Notes in Computer Science; Vol. 7679).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - An Executable Semantics for CompCert C

AU - Campbell, Brian

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-35308-6_8

DO - 10.1007/978-3-642-35308-6_8

M3 - Conference contribution

SN - 978-3-642-35307-9

T3 - Lecture Notes in Computer Science

SP - 60

EP - 75

BT - Certified Programs and Proofs

A2 - Hawblitzel, Chris

A2 - Miller, Dale

PB - Springer

ER -

An Executable Semantics for CompCert C

Abstract / Description of output

Publication series

Access to Document

Fingerprint

Cite this