Algebraic separation logic
type: Item
instance of: scholarly article
title: Algebraic separation logic
zbMATH Open document ID: 1260.03060
author: Peter Höfner
author: Bernhard Möller
author: Han-Hing Dang
published in: The Journal of Logic and Algebraic Programming
publication date: 2011-07-18T00:00:00Z
review text: Separation logic is an extension of Hoare logic with reasoning about complex and shared data structures by added assertions to express separation between memory regions. For arbitrary assertions \( p\) and \(q\) the conjunction \(p \star q\) asserts that \(p\) and \(q\) both hold, but each for separate parts of the storage, and \(p-\star q\) holds for a region if (roughly) \(p\) holds in another region then \(q\) holds in joint region of these two regions. In this paper an algebraic approach to separation logic is presented. In particular, an algebraic characterization for assertions of separation logic is given and different classes of assertions are discussed. A relational semantics of the commands of a simple programming language associated with separation logic is given by the presented algebraic framework. It is shown how to algebraically formulate the requirement that a command preserves certain variables. It is claimed that the algebraic view does not only yield new insights into separation logic but also shortens proofs due to a point-free representation.
reviewed by: Damas Gruska
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 5925505
zbMATH Keywords: Hoare logic
zbMATH Keywords: separation logic
zbMATH Keywords: standard Kleene algebra
zbMATH Keywords: programming language
zbMATH Keywords: semantics
describes a project that uses: Prover9
describes a project that uses: Mace4
describes a project that uses: Waldmeister
MaRDI profile type: Publication
full work available at URL: j.jlap.2011.04.003
OpenAlex ID: W2125806630
cites work: Refinement Calculus
cites work: Demonic operators and monotype factors
cites work: Q5532570
cites work: Q4056047
cites work: Q5674963
cites work: Q5639639
cites work: Embedding a demonic semilattice in a relation algebra
cites work: Q4362886
cites work: Characterizing determinacy in Kleene algebras
cites work: Kleene under a modal demonic star
cites work: Q4144755
cites work: Relational and Kleene-Algebraic Methods in Computer Science
cites work: An axiomatic basis for computer programming
cites work: Concurrent Kleene Algebra
cites work: Foundations of Concurrent Kleene Algebra
cites work: Automated Reasoning in Kleene Algebra
cites work: Automated verification of refinement laws
cites work: BI as an assertion language for mutable data structures
cites work: Boolean Algebras with Operators. Part I
cites work: On Hoare logic and Kleene algebra with tests
cites work: Q4428704
cites work: Q2767087
cites work: Relation algebras
cites work: Towards pointer algebra
cites work: Calculating with acyclic and cyclic lists
cites work: Kleene getting lazy
cites work: Quantales and Temporal Logics
cites work: Algebras of modal operators and partial correctness
cites work: Relational Methods in Computer Science
cites work: Q3771067
cites work: A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS
cites work: Resources, concurrency, and local reasoning
cites work: Q4783297
cites work: Frame rule for mutually recursive procedures manipulating pointers
cites work: Possible worlds and resources: The semantics of \(\mathbf{BI}\)
cites work: Q3996704
cites work: Q5287518
cites work: A Marriage of Rely/Guarantee and Separation Logic
cites work: Q4738240
DOI: 10.1016/J.JLAP.2011.04.003
description: scientific article; zbMATH DE number 5925505