A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Abstract elided by the publisher.
Related papers
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017
- Model checking for symbolic-heap separation logic with inductive predicates POPL 2016
- Strong-separation Logic TOPLAS 2022
- Strong-Separation Logic ESOP 2021
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Deciding Boolean Separation Logic via Small Models TACAS 2024
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic APLAS 2016
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ESOP 2017