### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Session GenClock

- GenClock

## Cite

×

GenClock-AFP

    @article{GenClock-AFP,
      author  = {Alwen Tiu},
      title   = {Formalization of a Generalized Protocol for Clock Synchronization},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2005},
      note    = {\url{https://isa-afp.org/entries/GenClock.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Nov 27, 2007 : Isabelle2007
- Oct 14, 2005 : Isabelle2005
- Jun 24, 2005 : Isabelle2004