Léon Gondelman
Radboud University
Semi-Automated Reasoning About Non-Determinism in C Expressions
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.
