A Logic-Based Framework for Verifying Consensus Algorithms

DOI10.1007/978-3-642-54013-4_10zbMath1428.68371OpenAlexW178138771MaRDI QIDQ2938065

Damien Zufferey, Helmut Veith, Josef Widder, Cezara Dragoi, 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)

Related Items (12)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Synthesis of distributed algorithms with parameterized threshold guards ⋮ Automated reasoning with restricted intensional sets ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Eliminating message counters in synchronous threshold automata ⋮ Reachability in Parameterized Systems: All Flavors of Threshold Automata ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Counting Constraints in Flat Array Fragments ⋮ Characterizing Consensus in the Heard-Of Model

This page was built for publication: A Logic-Based Framework for Verifying Consensus Algorithms