“Computer-assisted verification of an algorithm for concurrent timestamps”

Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco, and Nancy A. Lynch

Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV), Reinhard Gotzhein and Jan Bredereke (editors), pages 29–44, Kaiserslautern, Germany, October 8–11, 1996. Chapman & Hall.

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.

Back to Publications of Stephen J. Garland