Semi-Automated Reasoning About Non-Determinism in C Expressions

Léon Gondelman

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called “sequence point violations”. Undefined behavior may cause a program to crash or to have arbitrary results, so it is essential to make sure that C programs are free of undefined behavior for any expression evaluation order.

Together with Dan Frumin and Robbert Krebbers, we have recently developed a concurrent separation logic with a verification condition generator for a semi-automated reasoning about non-determinism in C expressions. The key novelty of our approach is a symbolic execution algorithm which is used to automatically determine how memory resources should be distributed among subexpressions.

In this talk I will explain our verification condition generator and symbolic executor, and how one can use them to reason about C programs within the Coq proof assistant.

---

Previous: Andrew Tolmach | Enforcing C-level security policies using machine-level tags
Next: Jonas Kastberg Hinrichsen | Building a Foundation for Verification of Distributed Systems in Iris