Rely-Guarantee Extensions and Locks

Robert J. Colvin, Scott Heiner, Peter Höfner 📧 and Roger C. Su 📧

November 21, 2025

Abstract

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.

License

BSD License

Topics

Related publications

  • Colvin, Heiner, Höfner and Su. Rely-guarantee concurrency verification of queued locks in Isabelle/HOL. VSTTE 2025.

Session RG_Locks

Cite

× 
@article{RG_Locks-AFP,
  author  = {Robert J. Colvin and Scott Heiner and Peter Höfner and Roger C. Su},
  title   = {Rely-Guarantee Extensions and Locks},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/RG_Locks.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download