Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
Abstract elided by the publisher.
Related papers
- Automatic cyclic termination proofs for recursive procedures in separation logic CPP 2017
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL 2026
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Automated lemma synthesis in symbolic-heap separation logic POPL 2018
- Cyclic proofs of program termination in separation logic POPL 2008
- Model checking for symbolic-heap separation logic with inductive predicates POPL 2016
- Model-guided synthesis of inductive lemmas for FOL with least fixpoints OOPSLA 2022
- Foundations for natural proofs and quantifier instantiation POPL 2018