Paul Eichler

Paul Eichler, Swen Jacobs, Chana Weil-Kennedy

We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to decide a wide range of verification problems, including control-state reachability, coverability, and target, in a fixed finite abstraction of the infinite state-space, called a 01-counter system. We show that several systems from the parameterized verification literature fall into this class, including reconfigurable broadcast networks (or systems with lossy broadcast), disjunctive systems, synchronizations and systems with a fixed number of shared finite-domain variables. Our framework provides a simple and unified explanation for the properties of these systems, which have so far been investigated separately. Additionally, it extends and improves on a range of the existing results, and gives rise to other systems with similar properties.

Paul Eichler, Tom Baumeister, Mouhammad Sakr et al.

We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.