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. 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 natural way.
CITATION STYLE
Nieto, L. P., & Esparza, J. (2000). Verifying single and multi-mutator garbage collectors with owicki-gries in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1893, pp. 619–628). Springer Verlag. https://doi.org/10.1007/3-540-44612-5_57
Mendeley helps you to discover research relevant for your work.