Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.

Leonor Prensa Nieto and Javier Esparza

As an aplication of the formalised Owicki/Gries method in the theorem prover Isabelle/HOL, we present the verification of a safety property for incremental garbage collection algorithms.

BibTeX: 

@InProceedings{  PrenEsp00-WS,
  author =       {L. Prensa Nieto and J. Esparza},
  title =        {Verifying garbage collection algorithms with {Owicki/Gries} in {Isabelle/HOL}},
  booktitle =    {Requirements, Design, Correct Construction and Verification},
  series=          {Softwaretechnik Reihe der Forschungsinstitut für Angewandte Softwaretechnologie},
  volume=          {11},
  pages =        {49--58},
  year =         {2000},
  editor =       {M.-V. Cengarle},
  publisher =    {Verlag Uni-Druck}
}