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