This is work done together with Jan Friso Groote of the CWI, from March to June 1998. It culminated in the paper W.H. Hesselink, J.F. Groote: Waitfree concurrent memory management by Create, and Read until Deletion (CaRuD). Dist. Comput. 14 (2001) 31-39.
The events files for the Nqthm proof of this
distributed algorithm are as follows.
The file crud0.events contains the modelling, the program, and the semantic lemmas.
The file crud1.events contains the constituent invariants.
The file crud2.events contains the construction of the global invariant, its proof of invariance, and the proof of its satisfiability, i.e. the initialization.
See the sibling directories for the methods used to handle sequential and distributed algorithms with Nqthm.