Verifying a distributed list system: A case history
Stein Krogdahl, Olav Lysne · Formal Aspects of Computing · 1997
Abstract The background for this paper is twofold: One is the definition of a caching protocol for shared memory parallel computers called SCI, and the other is the usage of rewriting techniques in program verification. The paper concentrates on a linked list system, which is a central aspect of the caching protocol. We first describe an informal proof of this system, including a rather large invariant. Thereafter we show how the list system and the invariant can both be described in the formalism of rewriting logic, and we use this to carry through a significant part of the verification mechanically, using the OBJ3 interpreter.