2026-07-22T21:39:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20751 2024-11-27T23:17:50Z ddc:004 open_access

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras Jackson, Vincent Murray, Toby Rizkallah, Christine verification concurrency rely-guarantee separation logic resource algebras This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vincent Jackson and Toby Murray and Christine Rizkallah 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.23 urn:nbn:de:0030-drops-207510 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23 eng https://creativecommons.org/licenses/by/4.0/legalcode