A decision procedure for satisfiability in separation logic with inductive predicates
DOI10.1145/2603088.2603091zbMATH Open1401.68111OpenAlexW2103490167WikidataQ130855327 ScholiaQ130855327MaRDI QIDQ4635608FDOQ4635608
James Brotherston, Juan Antonio Pérez, Nikos Gorogiannis, Carsten Fuhs
Publication date: 23 April 2018
Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2603088.2603091
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
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)
Cited In (22)
- Compositional satisfiability solving in separation logic
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
- Title not available (Why is that?)
- Separation logics and modalities: a survey
- Title not available (Why is that?)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- The SAT-based approach to separation logic
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
- Two-Variable Separation Logic and Its Inner Circle
- Unifying decidable entailments in separation logic with inductive definitions
- Separation logic with one quantified variable
- Compositional entailment checking for a fragment of separation logic
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Testing the satisfiability of formulas in separation logic with permissions
- SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
- Separation logic with linearly compositional inductive predicates and set data constraints
- On Temporal and Separation Logics
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)
