Verifying a garbage collection algorithm

We present a case study in using the PVS interactive theorem prover to formally model and verify properties of a tricolour garbage collection algorithm. We model the algorithm using state transition systems and verify safety and liveness properties in linear temporal logic. We set up two systems, each of which models the algorithm itself, object allocation, and the behaviour of user programs. The models differ in how concretely they model the heap. We verify the properties of the more abstract system, and then, once a refinement relation is exhibited between the systems, we show the more concrete system to have corresponding properties. We discuss the linear temporal logic framework we set up, commenting in particular an how we handle fairness and how we use a 'leads-to-via' predicate to reason about the propagation of properties that are stable in specified regions of system state spaces. We also describe strategies (tactics) we wrote to improve the quality of interaction and increase the degree of automation.