Mechanical Verification of a Constructive Proof for FLP
DOI10.1007/978-3-319-43144-4_7zbMATH Open1478.68146OpenAlexW2491855952MaRDI QIDQ2829253FDOQ2829253
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
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
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 (3)
Uses Software
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)
