Errors in published proofs

Mark Aagaard (aagaard@troy.cs.ubc.ca)
Tue, 22 Nov 1994 15:53:03 -0800

Rushby and von Henke used EHDM to verify Lamport's Interactive
Convergence Clock Synchronization Algorithm [LMS86]. While using EHDM
they found errors in four out of five lemmas and the main theorem
[RvH93]. As an example error, the inductive step in Lamport's proof
yields an ``aproximate inequality'', but the main theorem uses a
strict inequality.

-mark aagaard
aagaard@cs.ubc.ca

LMS86
Lamport, Leslie, and Melliar-Smith, P. M.
BYZANTINE CLOCK SYNCHRONIZATION.
Operating Systems Review (ACM) Oper Syst Rev (ACM) v 20 n 3
Jul 1986 p 10-16 1986, ISSN 0163-5980,

@article{RvH93,
author = {Rushby, John and von Henke, Friedrich},
title = {Formal Verification of Algorithms for Critical Systems},
journal = IEEE Transactions on Software Engineering
volume = 19,
number = 1
year = 1993,
month = jan,
pages = {13-23}
}