An Operational and Axiomatic Semantics for Non-determinism and Sequence

The C11 standard of the C programming language does not specify the execution order of expressions. Besides, to make more effective optimizations possible (e.g. delaying of side-effects and interleav-ing), it gives compilers in certain cases the freedom to use even more behaviors than just those of all execution orders. Widely used C compilers actually exploit this freedom given by the C standard for optimizations, so it should be taken seriously in formal verification. This paper presents an operational and ax-iomatic semantics (based on separation logic) for non-determinism and sequence points in C. We prove soundness of our axiomatic se-mantics with respect to our operational semantics. This proof has been fully formalized using the Coq proof assistant