Verification of consensus algorithms using satisfiability solving
From MaRDI portal
Publication:658669
DOI10.1007/S00446-010-0123-3zbMATH Open1231.68164OpenAlexW2046131303MaRDI QIDQ658669FDOQ658669
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
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
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Distributed systems (68M14)
Cites Work
- Formal Modeling and Analysis of Timed Systems
- Title not available (Why is that?)
- Unreliable failure detectors for reliable distributed systems
- Title not available (Why is that?)
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Impossibility of distributed consensus with one faulty process
- Bounded model checking using satisfiability solving
- Round-by-round fault detectors (extended abstract), unifying synchrony and asynchrony
- Title not available (Why is that?)
- The Heard-Of model: computing in distributed systems with benign faults
- Fast Paxos
- A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
- Using Bounded Model Checking to Verify Consensus Algorithms
- Title not available (Why is that?)
- Computer Aided Verification
Cited In (10)
- Characterizing Consensus in the Heard-Of Model
- Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
- Model Checking of Robot Gathering
- Title not available (Why is that?)
- Formal verification of mobile robot protocols
- Using Bounded Model Checking to Verify Consensus Algorithms
- Title not available (Why is that?)
- Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
Uses Software
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)
