Skip to Main content Skip to Navigation
Journal articles

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 metadata

Cited literature [45 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Tuesday, January 13, 2009 - 11:44:48 AM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
Long-term archiving on: : Tuesday, June 8, 2010 - 7:48:27 PM


Files produced by the author(s)




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⟩



Record views


Files downloads