A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs
No abstract available.
Related papers
- Deciding Boolean Separation Logic via Small Models TACAS 2024
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures VMCAI 2007
- Predicate Abstraction for Linked Data Structures VMCAI 2016
- Modular reasoning about heap paths via effectively propositional formulas POPL 2014
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ESOP 2017
- Predicate Abstraction via Symbolic Decision Procedures CAV 2005
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Deciding memory safety for single-pass heap-manipulating programs POPL 2020