HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Other publications

A Formalization of a Generalized Clock Synchronization Protocol in Isabelle/HOL

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 formalize the generalized Byzantine fault-tolerant clock synchronization protocol of Schneider. This protocol abstracts from particular algorithms or implementations for clock synchronization. This abstraction includes several assumptions on the behaviors of physical clocks and on general properties of concrete algorithms/implementations. Based on these assumptions the correctness of the protocol is proved by Schneider. His proof was later verified by Shankar using the theorem prover EHDM (precursor to PVS). Our formalization in Isabelle/HOL is based on Shankar's formalization.
Document type :
Other publications
Complete list of metadata

Contributor : Leonor Prensa Nieto Connect in order to contact the contributor
Submitted on : Friday, September 29, 2006 - 9:38:36 AM
Last modification on : Friday, February 4, 2022 - 3:30:21 AM


  • HAL Id : inria-00102104, version 1



Alwen Tiu. A Formalization of a Generalized Clock Synchronization Protocol in Isabelle/HOL. 2005. ⟨inria-00102104⟩



Record views