Verifying Single and Multi-mutator Garbage Collectors
with Owicki-Gries in Isabelle/HOL.
Leonor Prensa Nieto and Javier Esparza
Using a formalization of the Owicki-Gries method in the
theorem prover Isabelle/HOL, we obtain mechanized correctness
proofs for two incremental garbage collection algorithms, the second
one parametric in the number of mutators. No full Owicki-Gries proofs
of these algorithms existed so far, and for the second algorithm no
mechanized proof at all.
The Owicki-Gries method allows to reason directly on
the program code; it also splits the proof into many
small goals, most of which are very simple, and can thus be proved
automatically. Thanks to Isabelle's facilities in dealing with syntax, the
formalization can be done in a very natural way.
dvi
ps
BibTeX:
@InProceedings{PrenEsp00,
author = {Prensa Nieto, Leonor and Javier Esparza},
title = {Verifying Single and Multi-mutator Garbage Collectors
with {Owicki/Gries} in {Isabelle/HOL}},
booktitle = {Mathematical Foundations of Computer Science (MFCS 2000)},
editor = {M. Nielsen and B. Rovan},
publisher = {Springer-Verlag},
series = {LNCS},
volume = 1893,
pages = {619--628},
year = 2000
}