[isabelle] New in the AFP: The impossibility of distributed consensus



Iâm happy to announce a beautiful new AFP entry from the Technical University of Berlin. Details below.

Larry Paulson


A Constructive Proof for FLP

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.

http://www.isa-afp.org/entries/FLP.shtml





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.