Frame Inference for Inductive Entailment Proofs in Separation Logic
No abstract available.
Related papers
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Automated lemma synthesis in symbolic-heap separation logic POPL 2018
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL 2026
- Resource-sensitive synchronization inference by abduction POPL 2012
- Proof-Directed Parallelization Synthesis by Separation Logic TOPLAS 2013
- Automated Verification of Shape and Size Properties Via Separation Logic VMCAI 2007
- A First-order Logic with Frames TOPLAS 2023
- A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic POPL 2022