A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
From MaRDI portal
Publication:5370906
DOI10.1145/3009837.3009860zbMath1380.68278arXiv1608.05327OpenAlexW3100822217MaRDI QIDQ5370906
No author found.
Publication date: 20 October 2017
Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1608.05327
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)
Related Items (14)
Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications ⋮ A case study on parametric verification of failure detectors ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Synthesis of distributed algorithms with parameterized threshold guards ⋮ Liveness in broadcast networks ⋮ \(\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 ⋮ Unnamed Item ⋮ Coefficient synthesis for threshold automata ⋮ Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems ⋮ Eliminating message counters in synchronous threshold automata ⋮ A reduction theorem for randomized distributed algorithms under weak adversaries ⋮ Reachability in Parameterized Systems: All Flavors of Threshold Automata ⋮ Characterizing Consensus in the Heard-Of Model
Uses Software
This page was built for publication: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
