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.

Journal of Automated Reasoning (2009)

Cited by in corpus (9)

• A formally verified compiler back-end
• Verified Low-Level Programming Embedded in F*
• Renaming Global Variables in C Mechanically Proved Correct
• Skeletal Semantics and their Interpretations
• Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems
• From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
• A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
• Safety-Critical Java: Level 2 in Practice
• Generic Approach to Certified Static Checking of Module-like Constructs