Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact)
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek R. Dreyer, Ori Lahav, Viktor Vafeiadis · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2017
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.