Sciweavers

VSTTE
2010
Springer

Reusable Verification of a Copying Collector

13 years 1 months ago
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.
Magnus O. Myreen
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where VSTTE
Authors Magnus O. Myreen
Comments (0)