An Operational And Axiomatic Semantics For Non-Determinism And Sequence Points In C
POPL(2014)
摘要
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 interleaving), 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 axiomatic semantics (based on separation logic) for non-determinism and sequence points in C. We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized using the Coq proof assistant.
更多查看译文
关键词
Operational Semantics,Separation Logic,C Verification,Interactive Theorem Proving,Coq
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络