Formal Verification of Consensus Algorithms in a Proof Assistant

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 10 mai 2018 - 02:06:51
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

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

407

Téléchargements de fichiers

213