Rely-Guarantee Extensions and Locks (Q7361472)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry RG_Locks
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Rely-Guarantee Extensions and Locks |
AFP entry RG_Locks |
Statements
21 November 2025
0 references
Robert J. Colvin
0 references
Scott Heiner
0 references
Peter Höfner
0 references
Roger C. Su
0 references
Rely-Guarantee Extensions and Locks (English)
0 references
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.
0 references
