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 metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/inria-00539899
Contributor : Stephan Merz <>
Submitted on : Thursday, November 25, 2010 - 2:42:43 PM
Last modification on : Wednesday, April 3, 2019 - 1:23:12 AM
Long-term archiving on : Thursday, March 10, 2011 - 12:53:46 PM

Files

sho-isabelle.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00539899, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

469

Files downloads

254