The CH2O formalization of ISO C11

By Robbert Krebbers, ICIS, Radboud University Nijmegen

This is an ongoing development. If you are looking for the Coq sources corresponding to specific papers, take a look here.

About

The CH2O project aims at formalizing novel features of the ISO C11 standard of the C programming language. CH2O provides an operational, executable, and axiomatic semantics for a significant fragment of C11.

Our recent paper A Typed C11 Semantics for Interactive Theorem Proving at CPP 2015 gives a good overview of the CH2O project.

Papers

  1. Robbert Krebbers. A Formal C11 Memory Model for Separation Logic. Draft.
  2. Robbert Krebbers and Freek Wiedijk. A Typed C11 Semantics for Interactive Theorem Proving. In CPP, pages 15-27, 2015.
  3. Robbert Krebbers. Separation algebras for C verification in Coq. In VSTTE, volume 8471 of LNCS, pages 150-166, 2014.
  4. Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP, volume 8558 of LNCS, pages 543-548, 2014.
  5. Robbert Krebbers. An operational and axiomatic semantics for non-determinism and sequence points in C. In POPL, pages 101-112, 2014.
  6. Robbert Krebbers. Aliasing restrictions of C11 formalized in Coq. In CPP, volume 8307 of LNCS, pages 50-65, 2013.
  7. Robbert Krebbers and Freek Wiedijk. Separation Logic for Non-local Control Flow and Block Scope Variables. In FoSSaCS, volume 7794 of LNCS, pages 257-272, 2013.
    Awarded best student contribution.
  8. Robbert Krebbers and Freek Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In CICM, volume 6824 of LNAI, pages 297-299, 2011.

Download

The most recent version of the Coq source code of this development can be downloaded here. Use:

  scons -j [num cores]

to compile the development. This yields an executable called ch2o that can be used to test the CH2O semantics against actual C source files.

Table of contents

Prelude

Finite maps

Type system and integers

Permissions and separation algebras

Memory model

Operational semantics

Refinements

Executable semantics

Separation logic