Semi-automatic Proofs about Object Graphs in Separation Logic
Holger Gast · Technische Universität Berlin – Universitätsbibliothek · 2012
Published correctness proofs of garbage collectors in separation logic to date depend on extensive manual, interactive formula manipulations. This paper shows that the approach of symbolic execution in separation logic, as first developed by Smallfoot, also encompasses reasoning about object graphs given by the reachability of objects. This approach yields semi-automatic proofs of two central garbage collection algorithms: Schorr-Waite graph marking and Cheney's collector. Our framework is developed as a conservative extension of Isabelle/HOL. Our verification environment re-uses the Simpl framework for classical Hoare logic.