Mechanical Verification of a Garbage Collector

13 years 8 months ago
Mechanical Verification of a Garbage Collector
Abstract. We describe how the PVS verification system has been used to verify a safety property of a garbage collection algorithm, originally suggested by Ben-Ari. The safety property basically says that "nothing but garbage is ever collected". Although the algorithm is relatively simple, its parallel composition with a "user" program that (nearly) arbitrarily modifies the memory makes the verification quite challenging. The garbage collection algorithm and its composition with the user program is regarded as a concurrent system with two processes working on a shared memory. Such concurrent systems can be encoded in PVS as state transition systems, very similar to the models of, for example, UNITY and TLA. The algorithm is an excellent test-case for formal methods, be they based on theorem proving or model checking. Various hand-written proofs of the algorithm have been developed, some of which are wrong. David Russinoff has verified the algorithm in the Boyer-Moore...
Klaus Havelund
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where IPPS
Authors Klaus Havelund
Comments (0)