Lecture Notes in Computer Science, Volume 571.
From Formal Techniques in Real-Time and Fault-Tolerant Systems.
Edited by J. Vytopil.
Springer-Verlag, Nijmegen, The Netherlands.
January, 1992.
Pages 217–236.

Schneider generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. We present a mechanical verification of Schneider's protocol leading to several significant clarifications and revisions. The verification was carried out with the Ehdm system developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm satisfies the requirements of Schneider's protocol. Our mechanical verification raises a number of issues regarding the verification of fault-tolerant, distributed, real-time protocols that are germane to the design of a special-purpose logic for such problems.

@inproceedings{ftrtft92-ns,
    AUTHOR = {Natarajan Shankar},
    TITLE = {Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization},
    BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
    YEAR = {1992},
    EDITOR = {{J.} Vytopil},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {571},
    PAGES = {217--236},
    ADDRESS = {Nijmegen, The Netherlands},
    MONTH = {jan},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/ftrtft92-ns/}
}

• ftrtft92-ns.dvi.gz
• ftrtft92-ns.ps.gz