Constructive Proof FLP (Q40546)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry FLP
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Constructive Proof FLP |
AFP entry FLP |
Statements
Benjamin Bisping
0 references
Paul-David Brodmann
0 references
Tim Jungnickel
0 references
Christina Rickmann
0 references
Henning Seidler
0 references
Anke Stüber
0 references
Arno Wilhelm-Weidner
0 references
Kirstin Peters
0 references
Uwe Nestmann
0 references
The impossibility of distributed consensus with one faulty process is a result with important consequences for real world distributed systems e.g., commits in replicated databases. Since proofs are not immune to faults and even plausible proofs with a profound formalism can conclude wrong results, we validate the fundamental result named FLP after Fischer, Lynch and Paterson. We present a formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen Völzer's paper "A constructive proof for FLP". In addition to the enhanced confidence in the validity of Völzer's proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization can also be reused for further proofs of properties of distributed systems.
0 references
18 May 2016
0 references
A Constructive Proof for FLP (English)
0 references
