Abstract:

In my PhD project I am developing a formal semantics of a significant  fragment of the C programming language as described by the C11 standard. In this talk I will give a brief overview of the main parts of this semantics.

A structured memory model based on trees to capture subtleties of  C11 that have not been addressed by others.

• A core C language with a small step operational semantics. The operational semantics is non-deterministic due to unspecified expression evaluation order.
• An explicit type system for the core language that enjoys type preservation and progress.
• A type sound translation of actual C programs into the core language.
• An executable semantics that is proven to be sound and complete with respect to the operational semantics.
• Extensions of separation logic to reason about subtle constructs in C like non-determinism in expressions, and gotos in the presence of  block scope variables.

All proofs are fully formalized using the Coq proof assistant. To explore all defined and undefined behaviors of actual C programs, we use Coq's extraction mechanism to obtain an interpreter that can compute a stream of finite sets of reachable states for a given program.