On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability

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

Mathematics Subject Classification ID

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