Skip to Main content Skip to Navigation
Conference papers

Formal C semantics: CompCert and the C standard

Abstract : We discuss the difference between a formal semantics of the C standard, and a formal semantics of an implementation of C that satisfies the C standard. In this context we extend the CompCert semantics with end-of-array pointers and the possibility to byte-wise copy objects. This is a first and necessary step towards proving that the CompCert semantics refines the formal version of the C standard that is being developed in the Formalin project in Nijmegen.
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00981212
Contributor : Xavier Leroy <>
Submitted on : Monday, April 21, 2014 - 5:04:41 PM
Last modification on : Thursday, March 5, 2020 - 4:50:09 PM
Long-term archiving on: : Monday, April 10, 2017 - 4:01:53 PM

File

Formal-C-CompCert.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Robbert Krebbers, Xavier Leroy, Freek Wiedijk. Formal C semantics: CompCert and the C standard. ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩. ⟨hal-00981212⟩

Share

Metrics

Record views

434

Files downloads

481