Skip navigation
Skip navigation

Verification of clock synchronization algorithms: Experiments on a combination of deductive tools

Barsotti, Damian; Prensa-Nieto, Leonor; Tiu, Alwen


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 [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the...[Show more]

CollectionsANU Research Publications
Date published: 2007
Type: Journal article
Source: Formal Aspects of Computing
DOI: 10.1007/s00165-007-0027-6


File Description SizeFormat Image
01_Barsotti_Verification_of_clock_2007.pdf2.08 MBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator