Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Abstract elided by the publisher.
Related papers
- Decision Procedure for Entailment of Symbolic Heaps with Arrays APLAS 2017
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic CAV 2017
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic VMCAI 2011
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL 2026
- Separation Logic with Monadic Inductive Definitions and Implicit Existentials APLAS 2015
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ESOP 2017