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
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

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.

Mots clés: formal verification; proof assistant; consensus algorithm

Domaines: Logique en informatique [cs.LO]

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⟩