A logic-based framework for verifying consensus algorithms

DOI10.1007/978-3-642-54013-4_10MaRDI QIDQ2938065zbMATH OpenOpenAlexFDO

Authors Cezara Drăgoi, Helmut Veith, Josef Widder, Damien Zufferey, Thomas A. Henzinger

Publication date 13 January 2015

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

Full work available at URL https://doi.org/10.1007/978-3-642-54013-4_10

Mathematics Subject Classification ID

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

Recommendations

• Using Bounded Model Checking to Verify Consensus Algorithms
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• Cutoff bounds for consensus algorithms
• Formal Verification of Distributed Algorithms
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms

Cited in

(21)

• Cardinality constraints for arrays (decidability results and applications)
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Higher-order quantifier elimination, counter simulations and fault-tolerant systems
• Eliminating message counters in synchronous threshold automata
• Automated reasoning with restricted intensional sets
• Counting constraints in flat array fragments
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• What you always wanted to know about model checking of fault-tolerant distributed algorithms
• Synthesis of distributed algorithms with parameterized threshold guards
• Using Bounded Model Checking to Verify Consensus Algorithms
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• Reachability in parameterized systems: all flavors of threshold automata
• Characterizing Consensus in the Heard-Of Model
• A Distributed Algorithm of Fault Recovery for Stateful Failover
• On Verifying Fault Tolerance of Distributed Protocols
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• Verification of randomized consensus algorithms under round-rigid adversaries
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Verification of threshold-based distributed algorithms by decomposition to decidable logics
• Synthesis of distributed agreement-based systems with efficiently-decidable verification
• Verification of consensus algorithms using satisfiability solving

This page was built for publication: A logic-based framework for verifying consensus algorithms

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