An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
Abstract elided by the publisher.
Related papers
- Deciding memory safety for single-pass heap-manipulating programs POPL 2020
- Cyclic program synthesis PLDI 2021
- Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs ESOP 2015
- Modular reasoning about heap paths via effectively propositional formulas POPL 2014
- Predicate Abstraction for Linked Data Structures VMCAI 2016
- Gradual verification of recursive heap data structures OOPSLA 2020
- Separation Logic Modulo Theories APLAS 2013
- A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs VMCAI 2006