An efficient cyclic entailment procedure in a fragment of separation logic
From MaRDI portal
Publication:6091213
Abstract: An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent. This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our procedure is efficient and does not require back-tracking; it uses normalisation rules that help avoid the introduction of disjunction in the consequent. Moreover, our decidable fragment is sufficiently expressive: It is based on compositional predicates and can capture a wide range of data structures, including sorted and nested list segments, skip lists with fast forward pointers, and binary search trees. We have implemented the proposal in a prototype tool and evaluated it over challenging problems taken from a recent separation logic competition. The experimental results confirm the efficiency of the proposed system.
Cites work
- A complete decision procedure for linearly compositional separation logic with data constraints
- A decidable fragment in separation logic with inductive predicates and arithmetic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- A decision procedure for string logic with quadratic equations, regular expressions and length constraints
- A separation logic with data: small models and automation
- Automated cyclic entailment proofs in separation logic
- Automated mutual explicit induction proof in separation logic
- Automated mutual induction proof in separation logic
- Automated Reasoning with Analytic Tableaux and Related Methods
- BI as an assertion language for mutable data structures
- Compositional entailment checking for a fragment of separation logic
- Compositional satisfiability solving in separation logic
- Compositional shape analysis by means of bi-abduction
- Computer Aided Verification
- Deciding entailments in inductive separation logic with tree automata
- Foundations for decision problems in separation logic with general inductive predicates
- Frame inference for inductive entailment proofs in separation logic
- On automated lemma generation for separation logic with inductive definitions
- Programming Languages and Systems
- Satisfiability modulo heap-based programs
- Separation logic modulo theories
- The tree width of separation logic with recursive definitions
- Tractability of separation logic with inductive definitions: beyond lists
- Tractable Reasoning in a Fragment of Separation Logic
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Unifying decidable entailments in separation logic with inductive definitions
Cited in
(5)- Tractable Reasoning in a Fragment of Separation Logic
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
- Deciding satisfiability for overlaid symbolic heaps
- Tractable and intractable entailment problems in separation logic with inductively defined predicates
- An EXPTIME-complete entailment problem in separation logic
This page was built for publication: An efficient cyclic entailment procedure in a fragment of separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091213)
