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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. <10.1007/s10817-009-9148-3>


https://hal.inria.fr/inria-00352524
Contributeur : Xavier Leroy <>
Soumis le : mardi 13 janvier 2009 - 11:44:48
Dernière modification le : mercredi 7 octobre 2015 - 01:16:40
Document(s) archivé(s) le : mardi 8 juin 2010 - 19:48:27

Fichiers

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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>

Partager

Métriques

Consultations de
la notice

236

Téléchargements du document

221