Reusable verification of a copying collector

Abstract

Garbage collectors are very hard to implement correctly due to their low-level manipulation of memory. In this paper, we construct a copying garbage collector which we have proved to be functionally correct. Our verification proof is structured as a sequence of refinements to aid clarity and proof reuse; it is the first to map implementations into three different machine languages and, unlike some noteworthy published proofs, our verified implementations of memory allocation handle termination and the 'out-of-memory' case properly. The work presented here has been developed in the HOL4 theorem prover. © 2010 Springer-Verlag Berlin Heidelberg.