Mechanized semantics for the clight subset of the C language

DOI10.1007/s10817-009-9148-3zbMath1185.68136arXiv0901.3619OpenAlexW3106373601MaRDI QIDQ2655325

Xavier Leroy, Sandrine Blazy

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0901.3619

zbMATH Keywords

operational semanticsformal proofthe Coq proof assistantmechanized semanticsthe C programming language

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Reasoning about iteration and recursion uniformly based on big-step semantics ⋮ A formally verified compiler back-end ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ A Concrete Memory Model for CompCert ⋮ The rewriting logic semantics project: a progress report ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Unnamed Item ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM ⋮ A Verified LL(1) Parser Generator ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ Ott: Effective tool support for the working semanticist ⋮ A Formalization of the C99 Standard in HOL, Isabelle and Coq ⋮ Translating Xd-C programs to MSVL programs ⋮ Concrete Memory Models for Shape Analysis ⋮ The Rewriting Logic Semantics Project: A Progress Report

Uses Software

• Coq
• CUTE
• Ott
• ML
• veriSoft
• Isabelle/HOL
• Frama-C
• cminor
• CIL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A high-level modular definition of the semantics of C\(_{\sharp}\)
• Towards verification of C programs: Axiomatic semantics of the C-kernel language
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Coinductive big-step operational semantics
• Isabelle/HOL. A proof assistant for higher-order logic
• A compiled implementation of strong reduction
• Towards a mechanized metatheory of standard ML
• Separation Logic for Small-Step cminor
• Extracting Purely Functional Contents from Logical Inductive Types
• Ott
• Formal certification of a compiler back-end or
• Separation Logic Semantics for Communicating Processes
• A Sound Semantics for OCaml light
• Logic for Programming, Artificial Intelligence, and Reasoning