Abstract
The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations. Our memory model and essential properties of it have been fully formalized using the Coq proof assistant. © Springer International Publishing 2013.
Cite
CITATION STYLE
Krebbers, R. (2013). Aliasing restrictions of C11 formalized in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8307 LNCS, pp. 50–65). https://doi.org/10.1007/978-3-319-03545-1_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
