| 
|
Quote: formally verified Byzantine failure clock synchronization with EHDM; difficult; found many errors, though none serious
topics >
all references >
references p-r >
Group:
program proving
Topic:
synchronized processing
Quotation Skeleton
In order to resolve our doubts concerning [Lamport and Melliar-Smith's JACM 1/85] analysis of ICA [Interactive convergence algorithm for Byzantine failure clock synchronization], we embarked on a formal verification … [ref]. … [p. 7] In total, we found that four of … and that the main induction was incorrect. … We found the formal verification of ICA to … [p. 12] Note that our corrections merely dot the … [in the corrected proof] is due to Lamport and Melliar-Smith. Google-1 Google-2
Copyright clearance needed for quotation.
Group: program proving (10 topics, 310 quotes)
Topic: synchronized processing (35 items)