Abstract of Paper

Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL
by 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.