A decision procedure for satisfiability in separation logic with inductive predicates
DOI10.1145/2603088.2603091zbMATH Open1401.68111OpenAlexW2103490167WikidataQ130855327 ScholiaQ130855327MaRDI QIDQ4635608FDOQ4635608
Authors: James Brotherston, Carsten Fuhs, Nikos Gorogiannis, Juan Antonio Pérez 
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 (28)
- Compositional satisfiability solving in separation logic
- Title not available (Why is that?)
- Disproving inductive entailments in separation logic via base pair approximation
- Separation logics and modalities: a survey
- 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
- On temporal and separation logics
- Decision problems in a logic for reasoning about reconfigurable distributed systems
- Two-Variable Separation Logic and Its Inner Circle
- Foundations for decision problems in separation logic with general inductive predicates
- Tractability of separation logic with inductive definitions: beyond lists
- The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates
- Unifying decidable entailments in separation logic with inductive definitions
- Decision procedures for region logic
- A decision procedure for separation logic in SMT
- Separation logic with one quantified variable
- Compositional entailment checking for a fragment of separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Satisfiability modulo heap-based programs
- 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
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Separation logic with linearly compositional inductive predicates and set data constraints
- Unified reasoning about robustness properties of symbolic-heap 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)
