Skip to Main content Skip to Navigation
Journal articles

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

Bernadette Charron-Bost 1 Stephan Merz 2 
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, October 26, 2009 - 8:52:46 AM
Last modification on : Friday, February 4, 2022 - 3:20:33 AM


  • HAL Id : inria-00426388, version 1



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⟩



Record views