Mechanical Verification of a Constructive Proof for FLP

DOI10.1007/978-3-319-43144-4_7zbMath1478.68146OpenAlexW2491855952MaRDI QIDQ2829253

Uwe Nestmann, Christina Rickmann, Tim Jungnickel, Anke Stüber, Arno Wilhelm-Weidner, Benjamin Bisping, Henning Seidler, Paul-David Brodmann, Kirstin Peters

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-43144-4_7

zbMATH Keywords

verificationdistributed systemsconsensusIsabelle/HOLformalizationFLP

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Reliability, testing and fault tolerance of networks and computer systems (68M15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Constructive Proof FLP ⋮ Mechanical Verification of a Constructive Proof for FLP

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• Nuprl
• Locales
• Archive Formal Proofs

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A constructive proof for FLP
• A counter-example to an algorithm for the generalized input--output construct of CSP
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanical Verification of a Constructive Proof for FLP
• Formal Verification of Distributed Algorithms
• An Effective Implementation for the Generalized Input-Output Construct of CSP
• Impossibility of distributed consensus with one faulty process

This page was built for publication: Mechanical Verification of a Constructive Proof for FLP