Verification of consensus algorithms using satisfiability solving

DOI10.1007/S00446-010-0123-3MaRDI QIDQ658669zbMATH OpenOpenAlexFDO

Authors Tatsuhiro Tsuchiya, A. Schiper

Publication date 6 February 2012

Published in Distributed Computing (Search for Journal in Brave)

Full work available at URL http://infoscience.epfl.ch/record/171619

zbMATH Keywords

consensusmodel checkingformal verificationfault-tolerant distributed algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Distributed systems (68M14)

Recommendations

• Using Bounded Model Checking to Verify Consensus Algorithms
• Formal verification of Multi-Paxos for distributed consensus
• Formal modeling and verification of Paxos based on Coq
• A logic-based framework for verifying consensus algorithms
• Failure Detection and Randomization: A Hybrid Approach to Solve Consensus

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 1973984 (Why is no real title available?)
• scientific article; zbMATH DE number 1796134 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Bounded model checking using satisfiability solving
• Computer Aided Verification
• Fast Paxos
• Formal Modeling and Analysis of Timed Systems
• Impossibility of distributed consensus with one faulty process
• Round-by-round fault detectors (extended abstract), unifying synchrony and asynchrony
• The Heard-Of model: computing in distributed systems with benign faults
• Unreliable failure detectors for reliable distributed systems
• Using Bounded Model Checking to Verify Consensus Algorithms

Cited in

(14)

• Characterizing Consensus in the Heard-Of Model
• Formal verification of Multi-Paxos for distributed consensus
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms
• scientific article; zbMATH DE number 7365811 (Why is no real title available?)
• Formal verification of mobile robot protocols
• Using Bounded Model Checking to Verify Consensus Algorithms
• scientific article; zbMATH DE number 1424027 (Why is no real title available?)
• Verification of distributed systems with the axiomatic system of MSVL
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• Automated verification of multi-party agreements and scheduling of sending messages in distributed ledger systems
• The consensus machine: formalising consensus in the presence of malign agents
• Model checking of robot gathering

Describes a project that uses

Uses Software

• NuSMV
• SPIN

This page was built for publication: Verification of consensus algorithms using satisfiability solving

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