Mechanical Verification of a Constructive Proof for FLP
type: Item
instance of: scholarly article
title: Mechanical Verification of a Constructive Proof for FLP
zbMATH Open document ID: 1478.68146
DOI: 10.1007/978-3-319-43144-4_7
author: Benjamin Bisping
author: Paul-David Brodmann
author: Tim Jungnickel
author: Christina Rickmann
author: Henning Seidler
author: Anke Stüber
author: Arno Wilhelm-Weidner
author: Kirstin Peters
author: Uwe Nestmann
published in: Interactive Theorem Proving
publication date: 2016-10-27T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M14
Mathematics Subject Classification ID: 68M15
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 6644739
zbMATH Keywords: formalization
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: verification
zbMATH Keywords: FLP
zbMATH Keywords: consensus
zbMATH Keywords: distributed systems
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Nuprl
describes a project that uses: Isabelle
describes a project that uses: HOL
describes a project that uses: Locales
describes a project that uses: Archive Formal Proofs
MaRDI profile type: MaRDI publication profile
full work available at URL: 978-3-319-43144-4 7
OpenAlex ID: W2491855952
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: An Effective Implementation for the Generalized Input-Output Construct of CSP
cites work: Impossibility of distributed consensus with one faulty process
cites work: Formal Verification of Distributed Algorithms
cites work: A counter-example to an algorithm for the generalized input--output construct of CSP
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: A constructive proof for FLP
Recommended article: A constructive proof for FLP
Recommended article: Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
Recommended article: Q3714047
Recommended article: Q3718680
Recommended article: Theorem Proving in Higher Order Logics
Recommended article: Q3685173
Recommended article: Toward mechanical methods for streamlining proofs
Recommended article: The machinery of consistency proofs
Recommended article: The Mechanical Verification of a DPLL-Based Satisfiability Solver
description: scientific article; zbMATH DE number 6644739