DARTS.3.2.15.pdf
- Filesize: 351 kB
- 2 pages
Document
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Volume: DARTS, Volume 3 (ECOOP 2017)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Germany license
- Publication Date: 2017-06-20
Artifact Description
Document Identifiers
Cite AsGet BibTex
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/DARTS.3.2.15
https://doi.org/10.4230/DARTS.3.2.15
Artifact
DARTS-3-2-15-artifact-dbdf8c863bb606643d8ec203012362e3.zip
(Filesize: 1.66 GB)
Abstract
This artifact provides the soundness proofs for the encodings in Iris the RSL and GPS logics, as well as the verification for all standard examples known to be verifiable in those logics. All of these proofs are formalized in Coq, which is the main content of this artifact. The formalization is provided in a virtual machine for the convenience of testing, but can also be built from source.
Keywords
- weak memory models
- release-acquire
- concurrency
- separation logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads