|
 
|
[BL09] Mechanized semantics for the Clight subset of the C language
Revue Internationale avec comité de lecture : Journal JAR, Journal of Automated Reasoning, vol. 43(3), pp. 263-288, 2009
motcle:
Résumé:
This article presents the formal semantics of a large subset of the C
language called Clight. Clight includes pointer arithmetic,
struct and union types, C loops and structured switch
statements. Clight is the source language of the CompCert
verified compiler. The formal semantics of Clight is a big-step
semantics that observes both terminating and diverging executions and
produces traces of input/output events. The formal semantics of
Clight is mechanized using the Coq proof assistant. In addition to
the semantics of Clight, this article describes its integration in
the CompCert verified compiler and several ways by which the
semantics was validated.
BibTeX
| @article { | |||
| BL09, | |||
| title | = | "{Mechanized semantics for the Clight subset of the C language}", | |
| author | = | "S. Blazy and X. Leroy", | |
| journal | = | "JAR, Journal of Automated Reasoning", | |
| year | = | 2009, | |
| volume | = | 43, | |
| number | = | 3, | |
| pages | = | "263-288", | |
| } | |||
