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.
Type de document :
Communication dans un congrès
Michael Backes and Ralf Küsters. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany. 2010
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00539899
Contributeur : Stephan Merz <>
Soumis le : jeudi 25 novembre 2010 - 14:42:43
Dernière modification le : jeudi 21 février 2019 - 14:02:02
Document(s) archivé(s) le : jeudi 10 mars 2011 - 12:53:46

Fichiers

sho-isabelle.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00539899, version 1

Collections

Citation

Henri Debrat, Bernadette Charron-Bost, Stephan Merz. Formal Verification of Consensus Algorithms in a Proof Assistant. Michael Backes and Ralf Küsters. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany. 2010. 〈inria-00539899〉

Partager

Métriques

Consultations de la notice

456

Téléchargements de fichiers

238