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

DOI10.1016/j.ic.2016.03.006zbMath1355.68176MaRDI 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 checking; computational models; Byzantine faults; fault-tolerant distributed algorithms

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68M15: Reliability, testing and fault tolerance of networks and computer systems

68W15: Distributed algorithms

Uses Software

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