A decision procedure for satisfiability in separation logic with inductive predicates
From MaRDI portal
Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Model checking for symbolic-heap separation logic with inductive predicates
- Satisfiability modulo heap-based programs
- A decision procedure for separation logic in SMT
Cited in
(36)- Compositional entailment checking for a fragment of separation logic
- A decision procedure for separation logic in SMT
- Unifying decidable entailments in separation logic with inductive definitions
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Separation logic with linearly compositional inductive predicates and set data constraints
- Compositional satisfiability solving in separation logic
- Separation logic with one quantified variable
- A complete decision procedure for linearly compositional separation logic with data constraints
- Decision procedures for region logic
- Two-Variable Separation Logic and Its Inner Circle
- Unified reasoning about robustness properties of symbolic-heap separation logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Disproving inductive entailments in separation logic via base pair approximation
- SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
- Separation logics and modalities: a survey
- Satisfiability modulo heap-based programs
- Decidability for entailments of symbolic heaps with arrays
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- On temporal and separation logics
- Tractability of separation logic with inductive definitions: beyond lists
- The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
- Foundations for decision problems in separation logic with general inductive predicates
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Testing the satisfiability of formulas in separation logic with permissions
- Deciding satisfiability for overlaid symbolic heaps
- The satisfiability problem in a separation logic of relations
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Expressiveness results for an inductive logic of separated relations
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- Entailment checking in separation logic with inductive definitions is 2-ExpTime hard
- An EXPTIME-complete entailment problem in separation logic
- Encoding Peano arithmetic in a minimal fragment of separation logic
- The SAT-based approach to separation logic
This page was built for publication: A decision procedure for satisfiability in separation logic with inductive predicates
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635608)
