Name
Abstract | ||
|---|---|---|
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. We apply morphisms to abstract atomicity, where a program verified under one resource is adapted to operate under another resource, thus facilitating proof reuse. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3360587 | Proceedings of the ACM on Programming Languages |
Keywords | Field | DocType |
Coq, Hoare/Separation Logics, Program Logics for Concurrency | Atomicity,Separation logic,Programming language,Computer science,Reuse,Concurrency,Algebraic structure,Theoretical computer science,Invariant (mathematics),State transition systems,Morphism | Journal |
Volume | Issue | Citations |
abs/1904.07136 | OOPSLA | 1 |
PageRank | References | Authors |
0.35 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Aleksandar Nanevski | 1 | 583 | 27.01 |
| Anindya Banerjee | 2 | 1324 | 70.68 |
| Germán Andrés Delbianco | 3 | 40 | 3.53 |
| Ignacio Fábregas | 4 | 1 | 0.35 |