The relationship between separation logic and implicit dynamic frames

DOI10.1007/978-3-642-19718-5_23MaRDI QIDQ3000593zbMATH OpenOpenAlexFDO

Authors Matthew J. Parkinson, Alexander J. Summers

Publication date 19 May 2011

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1203.6859

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at first-order tool support. In this paper, we precisely connect the semantics of these two logics. We define a logic whose syntax subsumes both that of a standard separation logic, and that of implicit dynamic frames as sub-syntaxes. We define a total heap semantics for our logic, and, for the separation logic subsyntax, prove it equivalent the standard partial heaps model. In order to define a semantics which works uniformly for both subsyntaxes, we define the novel concept of a minimal state extension, which provides a different (but equivalent) definition of the semantics of separation logic implication and magic wand connectives, while also giving a suitable semantics for these connectives in implicit dynamic frames. We show that our resulting semantics agrees with the existing definition of weakest pre-condition semantics for the implicit dynamic frames fragment. Finally, we show that we can encode the separation logic fragment of our logic into the implicit dynamic frames fragment, preserving semantics. For the connectives typically supported by tools, this shows that separation logic can be faithfully encoded in a first-order automatic verification tool (Chalice).

Recommendations

• The relationship between separation logic and implicit dynamic frames
• Computer Science Logic
• Separation Logic for Higher-Order Store
• Relational separation logic
• Abstract dynamic frames

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• BI as an assertion language for mutable data structures
• Dafny: an automatic program verifier for functional correctness
• Permission accounting in separation logic
• Separation Logic for Small-Step cminor

Cited in

(8)

• WP semantics and behavioral subtyping
• Verifying Whiley programs with Boogie
• Bringing Order to the Separation Logic Jungle
• Abstract dynamic frames
• Generalized arrays for Stainless frames
• Frame problem in dynamic logic
• A first-order logic with frames
• The relationship between separation logic and implicit dynamic frames

Describes a project that uses

Uses Software

• cminor
• Boogie
• Dafny

This page was built for publication: The relationship between separation logic and implicit dynamic frames

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000593)