Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Abstract elided by the publisher.
Related papers
- Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution) TACAS 2012
- Predator: A Tool for Verification of Low-Level List Manipulation - (Competition Contribution) TACAS 2013
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- SLING: using dynamic analysis to infer program invariants in separation logic PLDI 2019
- Natural proofs for data structure manipulation in C using separation logic PLDI 2014
- Gradual C0: Symbolic Execution for Gradual Verification TOPLAS 2024
- Separation logic + superposition calculus = heap theorem prover PLDI 2011
- Cyclic program synthesis PLDI 2021