Verifying a Garbage Collection Algorithm (TPHOLs'98 paper)

Abstract for:
Paul B. Jackson. Verifying a Garbage Collection Algorithm. In Malcolm Newey and Jim Grundy editors, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '98). Canberra, Australia, September 1998. Vol 1479, Lecture Notes in Computer Science, Springer-Verlag.

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

BibTeX Entry:

@InProceedings{Jackson98:GCVerif,
  author = 	 {Paul B. Jackson},
  title = 	 {Verifying a Garbage Collection Algorithm},
  booktitle = 	 {11th International Conference on Theorem Proving in 
                  Higher-Order Logics: TPHOLs'98},
  editor =	 {Jim Grundy and Malcolm Newey},
  volume =	 {1479},
  series =	 {Lecture Notes in Computer Science},
  year =	 1998,
  publisher =	 {Springer-Verlag},
  month =	 {September},
  pages =	 {225--244}
}

Last Modified 7th October 1998