Skip to Main content Skip to Navigation
Journal articles

Formal Verification of a Consensus Algorithm in the Heard-Of Model

Abstract : Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.
Complete list of metadata

https://hal.inria.fr/inria-00426388
Contributor : Stephan Merz <>
Submitted on : Monday, October 26, 2009 - 8:52:46 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM

Identifiers

  • HAL Id : inria-00426388, version 1

Collections

Citation

Bernadette Charron-Bost, Stephan Merz. Formal Verification of a Consensus Algorithm in the Heard-Of Model. International Journal of Software and Informatics (IJSI), ISCAS, 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303. ⟨inria-00426388⟩

Share

Metrics

Record views

281