Computer-assisted verification of an algorithm for concurrent timestamps
Tsvetomir P. Petrov, Anna Pogosyants, Stephen J. Garland,
Victor Luchangco, and Nancy A. Lynch
Formal Description Techniques IX: Theory, Applications, and Tools (Reinhard
Gotzhein and Jan Bredereke, editors), Chapman & Hall, 1996, pages 29-44.
FORTE/PSTV '96: Joint International Conference on Formal
Description Techniques for Distributed Systems and Communication Protocols, and
Protocol Specification, Testing, and Verification,
Kaiserslautern, Germany, October 8-11, 1996
Abstract
A formal representation and machine-checked proof are given for the Bounded
Concurrent Timestamp (BCTS) algorithm of Dolev and Shavit. The proof uses
invariant assertions and a forward simulation mapping to a corresponding
Unbounded Concurrent Timestamp (UCTS) algorithm, following a strategy developed
by Gawlick, Lynch, and Shavit. The proof was produced interactively, using the
Larch Prover.