Email Gateway (Nov 21 2025 at 15:47): Email Gateway (Nov 21 2025 at 15:47):From: Tobias Nipkow <nipkow@in.tum.de>
Rely-Guarantee Extensions and Locks
Robert J. Colvin, Scott Heiner, Peter Höfner and Roger C. Su
We enhance rely-guarantee verification in Isabelle/HOL by extending the 2003
built-in library with flexible syntax, data-invariant support, and new tactics.
We demonstrate our enhanced library by applying it to the examples attached to
the original library. We also apply our library to three queue locks: the
Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.
https://www.isa-afp.org/entries/RG_Locks.html
Enjoy!
Last updated: Dec 02 2025 at 16:32 UTC