Algebraic separation logic
From MaRDI portal
Publication:549676
DOI10.1016/j.jlap.2011.04.003zbMath1260.03060OpenAlexW2125806630MaRDI QIDQ549676
Peter Höfner, Bernhard Möller, Han-Hing Dang
Publication date: 18 July 2011
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2011.04.003
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (14)
A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Developments in concurrent Kleene algebra ⋮ Transitive Separation Logic ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ The $$\theta $$-Join as a Join with $$\theta $$ ⋮ Exploring modal worlds ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Effect algebras, Girard quantales and complementation in separation logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Algebra of Monotonic Boolean Transformers ⋮ Modal algebra and Petri nets ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra ⋮ Extended transitive separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Embedding a demonic semilattice in a relation algebra
- Towards pointer algebra
- Frame rule for mutually recursive procedures manipulating pointers
- Kleene under a modal demonic star
- Algebras of modal operators and partial correctness
- Relation algebras
- Kleene getting lazy
- Resources, concurrency, and local reasoning
- Automated verification of refinement laws
- Characterizing determinacy in Kleene algebras
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Calculating with acyclic and cyclic lists
- Concurrent Kleene Algebra
- A Marriage of Rely/Guarantee and Separation Logic
- Automated Reasoning in Kleene Algebra
- Quantales and Temporal Logics
- Foundations of Concurrent Kleene Algebra
- A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS
- Demonic operators and monotype factors
- Refinement Calculus
- BI as an assertion language for mutable data structures
- An axiomatic basis for computer programming
- Relational and Kleene-Algebraic Methods in Computer Science
- On Hoare logic and Kleene algebra with tests
- Boolean Algebras with Operators. Part I
- Relational Methods in Computer Science
This page was built for publication: Algebraic separation logic
