TY - GEN
T1 - Verifying single and multi-mutator garbage collectors with owicki-gries in Isabelle/HOL
AU - Nieto, Leonor Prensa
AU - Esparza, Javier
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000
Y1 - 2000
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84959211211&partnerID=8YFLogxK
U2 - 10.1007/3-540-44612-5_57
DO - 10.1007/3-540-44612-5_57
M3 - Conference contribution
AN - SCOPUS:84959211211
SN - 3540679014
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 619
EP - 628
BT - Mathematical Foundations of Computer Science 2000 - 25th International Symposium, MFCS 2000 , Proceedings
A2 - Rovan, Branislav
A2 - Nielsen, Mogens
PB - Springer Verlag
T2 - 25th International Symposium on Mathematical Foundations of Computer Science, MFCS 2000
Y2 - 28 August 2000 through 1 September 2000
ER -