Mechanical Verification of a Constructive Proof for FLP

DOI10.1007/978-3-319-43144-4_7zbMATH Open1478.68146OpenAlexW2491855952MaRDI QIDQ2829253FDOQ2829253

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

verificationconsensusdistributed systemsIsabelle/HOLformalizationFLP

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

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

Uses Software

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

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Theorem Proving in Higher Order Logics 👍 👎
• The Mechanical Verification of a DPLL-Based Satisfiability Solver 👍 👎
• A constructive proof for FLP 👍 👎
• The machinery of consistency proofs 👍 👎
• Toward mechanical methods for streamlining proofs 👍 👎
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829253)