Email Gateway (Oct 16 2026 at 14:01): Email Gateway (Oct 16 2026 at 14:01):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Rely-Guarantee Specification of a Concurrent Garbage Collector
Rely-Guarantee Specification of a Concurrent Garbage Collector
Roger C. Su and Nisansala P. Yatapanage
We specify a model of the Ben-Ari concurrent garbage collector in the
rely-guarantee paradigm, and verify its correctness. The aim is to show that the
algorithm can be verified with rely-guarantee without the use of shared
auxiliary variables. The approach is to reason that a certain property is
maintained by one component for all instances of a variable, and then
instantiate it to the particular instance required by the rely of the other
component.
https://isa-afp.org/entries/RG_VDM_Garbage_Collector.html
Enjoy!
Last updated: Oct 29 2026 at 04:52 UTC