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”. These aspects should be accounted for in verification because C compilers exploit them. We present a verification condition generator (vcgen) that enables one to semi-automatically prove the absence of undefined behavior in a given C program for any evaluation order. The key novelty of our approach is a symbolic execution algorithm that computes a frame at the same time as a postcondition. The frame is used to automatically determine how resources should be distributed among subexpressions. We prove correctness of our vcgen with respect to a new monadic definitional semantics of a subset of C. This semantics is modular and gives a concise account of non-determinism in C. We have implemented our vcgen as a tactic in the Coq interactive theorem prover, and have proved correctness of it using a separation logic for the new monadic definitional semantics of a subset of C.
|Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|28th European Symposium on Programming, ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
|6/04/19 → 11/04/19