On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
From MaRDI portal
Publication:3190113
DOI10.1007/978-3-662-44584-6_10zbMath1417.68136OpenAlexW200623142MaRDI QIDQ3190113
No author found.
Publication date: 15 September 2014
Published in: CONCUR 2014 – Concurrency Theory (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.872.3003
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (8)
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 ⋮ \(\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 ⋮ An automata-theoretic approach to the verification of distributed algorithms ⋮ 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
This page was built for publication: On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability