Mechanized semantics for the Clight subset of the C language

Abstract : 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 operational 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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [45 references]  Display  Hide  Download

https://hal.inria.fr/inria-00352524
Contributor : Xavier Leroy <>
Submitted on : Tuesday, January 13, 2009 - 11:44:48 AM
Last modification on : Monday, May 13, 2019 - 10:46:04 AM
Long-term archiving on : Tuesday, June 8, 2010 - 7:48:27 PM

Files

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩. ⟨inria-00352524⟩

Share

Metrics

Record views

412

Files downloads

391