GRASShopper - Complete Heap Verification with Mixed Specifications
Abstract elided by the publisher.
Related papers
- Sound and Complete Invariant-Based Heap Encodings OOPSLA 2026
- Modular reasoning about heap paths via effectively propositional formulas POPL 2014
- The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code PLDI 2007
- FO-Complete Program Verification for Heap Logics OOPSLA 2025
- Model checking for symbolic-heap separation logic with inductive predicates POPL 2016
- Back to the future: revisiting precise program verification using SMT solvers POPL 2008
- Gradual C0: Symbolic Execution for Gradual Verification TOPLAS 2024
- Verification-Preserving Inlining in Automatic Separation Logic Verifiers OOPSLA 2023