| Formal Verification of a Consensus Algorithm in the Heard-Of Model |
| Received:March 05, 2009 Revised:August 10, 2009 Download PDF |
| Bernadette,Charron-Bost,Stephan Merz. Formal Verification of a Consensus Algorithm in the Heard-Of Model. International Journal of Software and Informatics, 2009,3(2):273~303 |
| Hits: 4128 |
| Download times: 3223 |
|
|
| 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. |
| keywords:formal verification theorem proving distributed algorithm Consensus fault-tolerance |
| View Full Text View/Add Comment Download reader |
