Using Bounded Model Checking to Verify Consensus Algorithms

DOI10.1007/978-3-540-87779-0_32zbMath1161.68586OpenAlexW1681015847MaRDI QIDQ3540251

Tatsuhiro Tsuchiya, André Schiper

Publication date: 20 November 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://infoscience.epfl.ch/record/125637/files/TR-07-2008.pdf

Mathematics Subject Classification ID

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

Related Items (5)

The Heard-Of model: computing in distributed systems with benign faults ⋮ Using Bounded Model Checking to Verify Consensus Algorithms ⋮ Verification of consensus algorithms using satisfiability solving ⋮ Formal Model–Driven Design of Distributed Algorithms ⋮ A Reduction Theorem for the Verification of Round-Based Distributed Algorithms

Uses Software

• NuSMV

Cites Work

• 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
• Impossibility of distributed consensus with one faulty process
• Unreliable failure detectors for reliable distributed systems
• Time is not a healer
• Disk Paxos
• Computer Aided Verification
• Formal Modeling and Analysis of Timed Systems
• Bounded model checking using satisfiability solving

This page was built for publication: Using Bounded Model Checking to Verify Consensus Algorithms