Reusable Verification of a Copying Collector

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.

• Type: Journal
• Year: 2010
• Where: VSTTE
• Authors: Magnus O. Myreen
• Keywords: Copying Garbage Collector, Garbage Collector, Noteworthy Published Proofs, Software Engineering, VSTTE 2010