| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Formalization of a Generalized Protocol for Clock Synchronization
| Title: | Formalization of a Generalized Protocol for Clock Synchronization |
| Author: | Alwen Tiu (ATiu /at/ ntu /dot/ edu /dot/ sg) |
| Submission date: | 2005-06-24 |
| 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. |
| BibTeX: |
@article{GenClock-AFP,
author = {Alwen Tiu},
title = {Formalization of a Generalized Protocol for Clock Synchronization},
journal = {Archive of Formal Proofs},
month = jun,
year = 2005,
note = {\url{http://isa-afp.org/entries/GenClock.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |