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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292043
Contributor : Sandrine Blazy <>
Submitted on : Monday, June 30, 2008 - 1:37:16 PM
Last modification on : Saturday, February 9, 2019 - 1:23:14 AM
Long-term archiving on : Friday, May 28, 2010 - 7:43:04 PM

File

C07Blazy.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00292043⟩

Share

Metrics

Record views

291

Files downloads

236