RT Conference Proceedings
T1 Specifying concurrent programs in separation logic: morphisms and simulations
A1 Nanevski, Aleksandar
A1 Banerjee, Anindya
A1 Delbianco, Germán Andrés
A1 Fábregas, Ignacio
A1 Fábregas Alfaro, Ignacio
AB In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resourcesÐa form of state transition systemsÐto describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.
YR 2019
FD 2019-10-01
LK https://hdl.handle.net/20.500.14352/98261
UL https://hdl.handle.net/20.500.14352/98261
LA eng
NO Nanevski A, Banerjee A, Delbianco GA, Fábregas I (2019) Specifying concurrent programs in separation logic: morphisms and simulations. Proc ACM Program Lang 3(OOPSLA):1–30. https://doi.org/10.1145/3360587
DS Docta Complutense
RD 6 abr 2025