Verification of consensus algorithms using satisfiability solving

DOI10.1007/s00446-010-0123-3zbMath1231.68164OpenAlexW2046131303MaRDI QIDQ658669

André Schiper, Tatsuhiro Tsuchiya

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

formal verificationmodel checkingconsensusfault-tolerant distributed algorithms

Mathematics Subject Classification ID

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

Related Items (6)

Formal verification of mobile robot protocols ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Model Checking of Robot Gathering ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Characterizing Consensus in the Heard-Of Model

Uses Software

• SPIN
• NuSMV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast Paxos
• The Heard-Of model: computing in distributed systems with benign faults
• Round-by-round fault detectors (extended abstract)
• Using Bounded Model Checking to Verify Consensus Algorithms
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• Impossibility of distributed consensus with one faulty process
• Unreliable failure detectors for reliable distributed systems
• Computer Aided Verification
• Formal Modeling and Analysis of Timed Systems
• Computer Aided Verification
• Bounded model checking using satisfiability solving

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