Algebraic separation logic
From MaRDI portal
Publication:549676
DOI10.1016/J.JLAP.2011.04.003zbMATH Open1260.03060OpenAlexW2125806630MaRDI QIDQ549676FDOQ549676
Authors: 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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Demonic operators and monotype factors
- Refinement Calculus
- BI as an assertion language for mutable data structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Boolean Algebras with Operators. Part I
- Embedding a demonic semilattice in a relation algebra
- Kleene under a modal demonic star
- An axiomatic basis for computer programming
- Relation algebras
- Title not available (Why is that?)
- Resources, concurrency, and local reasoning
- Title not available (Why is that?)
- Automated verification of refinement laws
- Title not available (Why is that?)
- Concurrent Kleene Algebra
- Automated Reasoning in Kleene Algebra
- Quantales and Temporal Logics
- Foundations of concurrent Kleene algebra
- On Hoare logic and Kleene algebra with tests
- Kleene getting lazy
- A Marriage of Rely/Guarantee and Separation Logic
- Title not available (Why is that?)
- Algebras of modal operators and partial correctness
- Title not available (Why is that?)
- Characterizing determinacy in Kleene algebras
- Calculating with acyclic and cyclic lists
- A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS
- Title not available (Why is that?)
- Title not available (Why is that?)
- Relational and Kleene-Algebraic Methods in Computer Science
- Relational Methods in Computer Science
- Towards pointer algebra
- Frame rule for mutually recursive procedures manipulating pointers
Cited In (28)
- Exploring modal worlds
- The $$\theta $$-Join as a Join with $$\theta $$
- On the relation between concurrent separation logic and concurrent Kleene algebra
- Algebra of monotonic Boolean transformers
- Looking at separation algebras with Boolean BI-eyes
- False failure: creating failure models for separation logic
- Stone-type dualities for separation logics
- Bringing Order to the Separation Logic Jungle
- Two for the price of one: lifting separation logic assertions
- Extended transitive separation logic
- Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Lightweight Separation
- Developments in concurrent Kleene algebra
- Extending separation logic with fixpoints and postponed substitution
- A stone-type duality theorem for separation logic via its underlying bunched logics
- Abstract dynamic frames
- Effect algebras, Girard quantales and complementation in separation logic
- Mechanised Separation Algebra
- Variable side conditions and greatest relations in algebraic separation logic
- Fictional separation logic
- An algebraic glimpse at bunched implications and separation logic
- A program construction and verification tool for separation logic
- Modal algebra and Petri nets
- Algebraic neighbourhood logic
- Separation logic for non-local control flow and block scope variables
- Towards algebraic separation logic
- Transitive Separation Logic
Uses Software
This page was built for publication: Algebraic separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q549676)
