Publications in Scientific Journals:
R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder:
"Decidability of Parameterized Verification";
ACM SIGACT News,
Parameterized model checking is an active research field that considers automated verification of distributed or concurrent systems, for all numbers of participating processes. In our
recent book  we surveyed literature on decidability of parameterized verification. The system
models, as well as the proof methods, that are studied in this field are similar to those from
distributed computing. For instance, we survey results for token passing systems and ad hoc
networks. The proof methods for undecidability include simulation of two-counter machines.
For decidability, we survey cut-off results that provide conditions to reduce parameterized verification to model checking of fixed-size systems. We believe that the results are of interest to
the readers of the Distributed Computing Column, and in this short note we want to give a
taste of parameterized model checking.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Project Head Igor Konnov:
Abstraction-based Parameterized TLA Checker
Project Head Josef Widder:
Parametrized Verification of Fault-tolerant Distributed Algorithms
Created from the Publication Database of the Vienna University of Technology.