Experiments in validating formal semantics for C

Abstract : This paper reports on the design of adequate on-machine formal semantics for a certified C compiler. This compiler is an optimizing compiler, that targets critical embedded software. It is written and formally verified using the Coq proof assistant. The main structure of the compiler is very strongly conditioned by the choice of the languages of the compiler, and also by the kind of semantics of these languages.
Type de document :
Communication dans un congrès
C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102, 2007
Liste complète des métadonnées


https://hal.inria.fr/inria-00292043
Contributeur : Sandrine Blazy <>
Soumis le : lundi 30 juin 2008 - 13:37:16
Dernière modification le : lundi 5 octobre 2015 - 16:58:58
Document(s) archivé(s) le : vendredi 28 mai 2010 - 19:43:04

Fichier

C07Blazy.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00292043, version 1

Collections

Citation

Sandrine Blazy. Experiments in validating formal semantics for C. C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102, 2007. <inria-00292043>

Partager

Métriques

Consultations de
la notice

197

Téléchargements du document

168