|
 
|
[BLA07a] Experiments in validating formal semantics for C
Conférence Internationale avec comité de lecture : C/C++ Verification Workshop, Oxford, United Kingdom, January 2007, pp.95-102, Series ICIS-R07015,
motcle:
Résumé:
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.
BibTeX
| @inproceedings { | |||
| BLA07a, | |||
| title | = | "{Experiments in validating formal semantics for C}", | |
| author | = | " S. Blazy ", | |
| booktitle | = | "{C/C++ Verification Workshop, Oxford, United Kingdom}", | |
| year | = | 2007, | |
| month | = | "January", | |
| series | = | "ICIS-R07015", | |
| pages | = | "95-102", | |
| } | |||
