Skip to Main content Skip to Navigation
New interface
Conference papers

Formal Verification of Consensus Algorithms in a Proof Assistant

Henri Debrat 1 Bernadette Charron-Bost 2 Stephan Merz 1 
1 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : Consensus is regarded as the fundamental problem that must be solved to implement a fault-tolerant distributed system. It requires nodes to eventually agree on a common value among the initial values held by each of them. Agreement should be reached despite the failures of some components (process or link). Depending on the timing and failure models, numerous Consensus algorithms have been proposed in the literature. We are studying techniques for proving the correctness of these algorithms using the interactive proof assistant Isabelle, aiming for a high level of automation.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Thursday, November 25, 2010 - 2:42:43 PM
Last modification on : Friday, February 4, 2022 - 3:20:33 AM
Long-term archiving on: : Thursday, March 10, 2011 - 12:53:46 PM


Files produced by the author(s)


  • HAL Id : inria-00539899, version 1



Henri Debrat, Bernadette Charron-Bost, Stephan Merz. Formal Verification of Consensus Algorithms in a Proof Assistant. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany. ⟨inria-00539899⟩



Record views


Files downloads