Verifying a garbage collection algorithm

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication11th International Conference, TPHOLs'98 Canberra, Australia September 27–October 1, 1998 Proceedings
EditorsJim Grundy, Malcolm Newey
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages20
ISBN (Print)978-3-540-64987-8, 978-3-540-49801-8
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Verifying a garbage collection algorithm'. Together they form a unique fingerprint.

Cite this