Existential Heap Abstraction Entailment Is Undecidable
Abstract elided by the publisher.
Related papers
- Decision Procedure for Entailment of Symbolic Heaps with Arrays APLAS 2017
- Foundations for Entailment Checking in Quantitative Separation Logic ESOP 2022
- Automated lemma synthesis in symbolic-heap separation logic POPL 2018
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines CPP 2019
- Decidable Subtyping of Existential Types for Julia PLDI 2024
- Separation logic + superposition calculus = heap theorem prover PLDI 2011
- Strong-Separation Logic ESOP 2021