Aliasing Restrictions of C11 Formalized in Coq
No abstract available.
DOI 10.1007/978-3-319-03545-1_4
Related papers
- A Typed C11 Semantics for Interactive Theorem Proving CPP 2015
- Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it POPL 2015
- Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris ECOOP 2017
- Formal Reasoning about the C11 Weak Memory Model CPP 2015
- A Type System for Effect Handlers and Dynamic Labels ESOP 2023
- HOπ in Coq CPP 2018
- Overhauling SC atomics in C11 and OpenCL POPL 2016
- A practical type system for safe aliasing SLE 2018