Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools

Damian Barsotti 1 Leonor Prensa Nieto 1 Alwen Tiu 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider's generalized clock synchronization protocol in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith~\cite{lamport_cs} and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch, satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify the parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetic like ICS and CVC Lite.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [16 references]  Display  Hide  Download
Contributor : Leonor Prensa Nieto <>
Submitted on : Thursday, November 10, 2005 - 2:01:26 PM
Last modification on : Thursday, January 11, 2018 - 6:19:52 AM
Document(s) archivé(s) le : Friday, April 2, 2010 - 6:56:19 PM


  • HAL Id : inria-00000638, version 1



Damian Barsotti, Leonor Prensa Nieto, Alwen Tiu. Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS '05, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK. ⟨inria-00000638⟩



Record views


Files downloads