HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292043
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Monday, June 30, 2008 - 1:37:16 PM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
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

155

Files downloads

151