




Publications  Verifying Single and Multimutator Garbage Collectors with OwickiGries in Isabelle/HOL





Reference:
L. Prensa Nieto and J. Esparza. Verifying single and multimutator garbage collectors with OwickiGries in Isabelle/HOL. In M. Nielsen and B. Rovan, editors, Proceedings of the 25th Conference on Mathematical Foundations of Computer Science, number 1893 in Lecture Notes in Computer Science, pages 619–628. SpringerVerlag, 2000.
Abstract:
Using a formalization of the OwickiGries 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 OwickiGries proofs of these algorithms existed so far, and for the second algorithm no mechanized proof at all. The OwickiGries 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.
Suggested BibTeX entry:
@inproceedings{PE00,
author = {L. Prensa Nieto and J. Esparza},
booktitle = {{Proceedings of the 25th~Conference on Mathematical Foundations of Computer Science}},
editor = {M. Nielsen and B. Rovan},
number = {1893},
pages = {619628},
publisher = {{SpringerVerlag}},
series = {{Lecture Notes in Computer Science}},
title = {Verifying Single and Multimutator Garbage Collectors with {O}wicki{G}ries in {I}sabelle/{HOL}},
year = {2000}
}




