Semi-automatic Proofs about Object Graphs in Separation Logic

Abstract

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.