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...

• Type: Conference
• Year: 1999
• Where: IPPS
• Authors: Klaus Havelund
• Keywords: Distributed And Parallel Computing, Garbage Collection Algorithm, IPPS 1999, PVS Verification, Safety Property