On the completeness of bounded model checking for threshold-based distributed algorithms: reachability

DOI10.1016/j.ic.2016.03.006zbMath1355.68176OpenAlexW2292447407MaRDI QIDQ729813

D. Kharzeev

Publication date: 22 December 2016

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2016.03.006

zbMATH Keywords

model checkingcomputational modelsByzantine faultsfault-tolerant distributed algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Reliability, testing and fault tolerance of networks and computer systems (68M15) Distributed algorithms (68W15)

Related Items (10)

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Model Checking of Robot Gathering ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Unnamed Item ⋮ Coefficient synthesis for threshold automata ⋮ 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 ⋮ Characterizing Consensus in the Heard-Of Model

Uses Software

• NuSMV
• Plingeling
• Treengeling
• FAST
• ByMC
• Lingeling

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An approach to automating the verification of compact parallel coordination programs. I
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Linear Completeness Thresholds for Bounded Model Checking
• Symbolic Counter Abstraction for Concurrent Software
• Asynchronous consensus and broadcast protocols
• Reaching Agreement in the Presence of Faults
• Reduction
• Time, clocks, and the ordering of events in a distributed system
• Unreliable failure detectors for reliable distributed systems
• Decidability of Parameterized Verification
• Automated Technology for Verification and Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability