2026-07-24T14:10:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7296 2024-03-06T11:05:01Z ddc:004 open_access

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Artifact) Kaiser, Jan-Oliver Dang, Hoang-Hai Dreyer, Derek Lahav, Ori Vafeiadis, Viktor weak memory models release-acquire concurrency separation logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan-Oliver Kaiser and Hoang-Hai Dang and Derek Dreyer and Ori Lahav and Viktor Vafeiadis 2017 Is Part Of DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.3.2.15 urn:nbn:de:0030-drops-72966 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.15 eng https://creativecommons.org/licenses/by/3.0/de/legalcode