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.
Type de document :
Communication dans un congrès
ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, 8558, pp.543-548, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-08970-6_36>
Liste complète des métadonnées

https://hal.inria.fr/hal-00981212
Contributeur : Xavier Leroy <>
Soumis le : lundi 21 avril 2014 - 17:04:41
Dernière modification le : mercredi 14 décembre 2016 - 01:07:25

Fichier

Formal-C-CompCert.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. Springer, 8558, pp.543-548, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-08970-6_36>. <hal-00981212>

Partager

Métriques

Consultations de
la notice

227

Téléchargements du document

180