D. Barsotti, Instances of schneider's generalized protocol of clock synchronization The Archive of Formal Proofs, 2006.

S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith et al., Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations, POPL'06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.55-66, 2006.

J. Botaschanjan, L. Kof, C. Kühnel, and M. Spichkova, Towards Verified Automotive Software, Proceedings of the 2nd International ICSE workshop on Software, 2005.

D. Barsotti, L. P. Nieto, and A. Tiu, Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools, Electronic Notes in Theoretical Computer Science, vol.145, pp.63-78, 2006.
DOI : 10.1016/j.entcs.2005.10.005
URL : https://hal.archives-ouvertes.fr/inria-00097383

L. A. Dennis, G. Collins, R. Boulton, K. Slind, G. Robinson et al., The PROSPER toolkit, Proceedings of TACAS'03, number 1785 in LNCSFle04] FlexRay Consortium. FlexRay Communications System Protocol Specification Version 2.0, pp.78-92, 2003.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088

C. Kühnel and M. Spichkova, FlexRay und FTCom: Formale Spezifikation in FOCUS, 2006.

J. Lundelius and N. Lynch, A new fault-tolerant algorithm for clock synchronization, Proceedings of the third annual ACM symposium on Principles of distributed computing , PODC '84, pp.75-88, 1984.
DOI : 10.1145/800222.806738

L. Lamport and P. M. Melliar-smith, Synchronizing clocks in the presence of faults, Journal of the ACM, vol.32, issue.1, pp.52-78, 1985.
DOI : 10.1145/2455.2457

S. Mclaughlin, C. Barrett, and Y. Ge, Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.43-51, 2006.
DOI : 10.1016/j.entcs.2005.12.005

P. S. Miner, Verification of fault-tolerant clock synchronization systems, NASA Technical Paper, vol.3349, 1993.

J. Meng and L. C. Paulson, Experiments on Supporting Interactive Proof Using Resolution, Lecture Notes in Computer Science, vol.3097, pp.372-384, 2004.
DOI : 10.1007/978-3-540-25984-8_28

T. Nipkow, Structured Proofs in Isar/HOL, Lecture Notes in Computer Science, vol.2646, pp.259-278, 2002.
DOI : 10.1007/3-540-39185-1_15

S. Ranise and C. Tinelli, The SMT-LIB standard : Version 1, 2005.

H. Jörg, C. Siekmann, V. Benzmüller, L. Brezhnev, A. Cheikhrouhou et al., Proof development with OMEGA, CADE, pp.144-149, 2002.

F. B. Schneider, Understanding protocols for Byzantine clock synchronization, 1987.

N. Shankar, Mechanical verification of a generalized protocol for Byzantine fault tolerant clock synchronization, Lecture Notes in Computer Science, vol.571, pp.217-236, 1992.
DOI : 10.1007/3-540-55092-5_12

D. Schwier and F. Henke, Mechanical verification of clock synchronization algorithms, Formal Techniques in Real-Time and Fault-Tolerant Systems, number 1486 in LNCS, pp.262-271, 1998.
DOI : 10.1007/BFb0055353

B. Tavernier, Calife: A Generic Graphical User Interface for Automata Tools, Electronic Notes in Theoretical Computer Science, vol.110, pp.169-172, 2004.
DOI : 10.1016/j.entcs.2004.06.004

A. Tiu, The Archive of Formal Proofs Formal proof development, 2005.

T. Weber, Integrating a SAT Solver with an LCF-style Theorem Prover, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.67-78, 2006.
DOI : 10.1016/j.entcs.2005.12.007