DARTS.6.2.4.pdf
- Filesize: 267 kB
- 3 pages
7e6f145f56db2f4952dc9cdcc77d28f6
(Get MD5 Sum)
The artifact is a virtual machine image containing two Coq packages which include mechanization of proofs stated in the paper. The first package imm contains a modified version of the Intermediate Memory Model, extended with the support of sequentially consistent atomics, and the compilation correctness proofs from it to hardware models. The second package weakestmoToImm contains a definition of the Weakestmo memory model as well as a compilation correctness proof from it to IMM.
Feedback for Dagstuhl Publishing