Mechanical proofs of fault-tolerant clock synchronization

The following topics are covered in viewgraph form: (1) introduction to clock synchronization protocols; (2) a schematic formulation of clock synchronization; (3) the interactive convergence algorithm; (4) verification of Schneider's formulation; (5) verification of interactive convergence; (6) a hardware-oriented clock synchronization protocol; (7) verification of Infis/Moore's protocol; and (8) the EHDM specification/verification environment.