Using Bounded Model Checking to Verify Consensus Algorithms

DOI10.1007/978-3-540-87779-0_32MaRDI QIDQ3540251zbMATH OpenOpenAlexFDO

Authors Tatsuhiro Tsuchiya, A. 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 algorithms (68W15) Distributed systems (68M14)

Recommendations

• Verification of consensus algorithms using satisfiability solving
• scientific article; zbMATH DE number 1796134
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• An automata-theoretic approach to the verification of distributed algorithms
• A logic-based framework for verifying consensus algorithms

Cites work

• scientific article; zbMATH DE number 1796134 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Bounded model checking using satisfiability solving
• Computer Aided Verification
• Disk paxos
• 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
• Time is not a healer (preliminary version)
• Unreliable failure detectors for reliable distributed systems
• Using Bounded Model Checking to Verify Consensus Algorithms

Cited in

(13)

• Formal model-driven design of distributed algorithms
• Model checking Paxos in Spin
• scientific article; zbMATH DE number 2087627 (Why is no real title available?)
• Formal modeling and verification of Paxos based on Coq
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• The Heard-Of model: computing in distributed systems with benign faults
• Using Bounded Model Checking to Verify Consensus Algorithms
• A method for the verification of a distributed and synchronized algorithm
• A logic-based framework for verifying consensus algorithms
• Verification of consensus algorithms using satisfiability solving
• An automata-theoretic approach to the verification of distributed algorithms
• scientific article; zbMATH DE number 1796134 (Why is no real title available?)
• Communication-closed asynchronous protocols

Describes a project that uses

Uses Software

• NuSMV

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

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