Mechanical Verification of a Constructive Proof for FLP

DOI10.1007/978-3-319-43144-4_7MaRDI QIDQ2829253zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• A constructive proof for FLP
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
• scientific article; zbMATH DE number 3941499
• scientific article; zbMATH DE number 3948225
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 3907752
• Toward mechanical methods for streamlining proofs
• The machinery of consistency proofs
• The mechanical verification of a DPLL-based satisfiability solver

Cites work

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

Cited in

(3)

• A constructive proof for FLP
• Mechanical Verification of a Constructive Proof for FLP
• Constructive Proof FLP

Describes a project that uses

Uses Software

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

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)