From owner-qed Tue Nov 22 17:54:50 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id RAA14546 for qed-out; Tue, 22 Nov 1994 17:53:44 -0600
Received: from grolsch.cs.ubc.ca (grolsch-2.cs.ubc.ca [142.103.5.5]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id RAA14541 for <qed@mcs.anl.gov>; Tue, 22 Nov 1994 17:53:39 -0600
Received: from troy.cs.ubc.ca (aagaard@troy.cs.ubc.ca [142.103.11.19]) by grolsch.cs.ubc.ca (8.6.9/8.6.9) with SMTP id PAA07882 for <qed@mcs.anl.gov>; Tue, 22 Nov 1994 15:53:06 -0800
Message-Id: <199411222353.PAA07882@grolsch.cs.ubc.ca>
From: aagaard@troy.cs.ubc.ca (Mark Aagaard)
Date: Tue, 22 Nov 1994 15:53:03 -0800
Reply-To: Mark Aagaard <aagaard@cs.ubc.ca>
Organization: University of British Columbia, Computer Science
X-Address: Vancouver, BC V6T 1Z4
X-Phone: 604/822-5401
X-Fax: 604/822-5485
X-Mailer: Mail User's Shell (7.2.4 2/2/92)
To: qed@mcs.anl.gov
Subject: Errors in published proofs
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


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}
}