Semi-Automated Reasoning About Non-Determinism in C Expressions

Léon Gondelman

Date: Wed, April 03, 2019
Time: 12:00

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 |
Next: Jonas Kastberg Hinrichsen |