Foundations for Decision Problems in Separation Logic with General Inductive Predicates

DOI10.1007/978-3-642-54830-7_27zbMath1406.03046OpenAlexW122465024MaRDI QIDQ5410687

Joël Ouaknine, Nikos Gorogiannis, Timos Antonopoulos, Christoph Haase, Max I. Kanovich

Publication date: 16 April 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54830-7_27

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (16)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Program Verification with Separation Logic ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Separation logic with one quantified variable ⋮ Separation logics and modalities: a survey ⋮ Unnamed Item ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Strong-separation logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Unifying decidable entailments in separation logic with inductive definitions ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• SLAyer

This page was built for publication: Foundations for Decision Problems in Separation Logic with General Inductive Predicates