Mechanized semantics for the Clight subset of the C language - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2009

Mechanized semantics for the Clight subset of the C language

(1, 2) , (2)
1
2

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.
Fichier principal
Vignette du fichier
paper.pdf (222.69 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00352524 , version 1 (13-01-2009)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More