## Robbert Krebbers, Xavier Leroy, and Freek Wiedijk.
Formal C semantics: CompCert and the C standard.
In *Interactive Theorem Proving, ITP 2014*, volume 8558 of *
Lecture Notes in Computer Science*, pages 543-548. Springer, 2014.

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.

[ bib |
At HAL |
Local copy |
At publisher's ]
Back

*This file was generated by
bibtex2html 1.97.*