Decision Procedure for Entailment of Symbolic Heaps with Arrays
From MaRDI portal
(Redirected from Publication:5055997)
Abstract: This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al, namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.
Recommendations
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- A decision procedure for separation logic in SMT
- On Symbolic Heaps Modulo Permission Theories
- Compositional entailment checking for a fragment of separation logic
- Compositional entailment checking for a fragment of separation logic
Cites work
- A decision procedure for satisfiability in separation logic with inductive predicates
- A Logic-Based Framework for Reasoning about Composite Data Structures
- Back to the future, revisiting precise program verification using SMT solvers
- Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
- Biabduction (and related problems) in array separation logic
- Compositional entailment checking for a fragment of separation logic
- Compositional invariant checking for overlaid and nested linked lists
- Compositional shape analysis by means of bi-abduction
- Deciding entailments in inductive separation logic with tree automata
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Foundations for decision problems in separation logic with general inductive predicates
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Programming Languages and Systems
- Separation logic with monadic inductive definitions and implicit existentials
- The tree width of separation logic with recursive definitions
- Tractable Reasoning in a Fragment of Separation Logic
- Verification, Model Checking, and Abstract Interpretation
Cited in
(3)
This page was built for publication: Decision Procedure for Entailment of Symbolic Heaps with Arrays
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055997)
