[Back]

R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder:
"Decidability of Parameterized Verification";
ACM SIGACT News, 47 (2016), 2; 53 - 64.

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 [11] 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.

http://dx.doi.org/10.1145/2951860.2951873

http://dl.acm.org/citation.cfm?doid=2951860.2951873

Project Head Igor Konnov:
Abstraction-based Parameterized TLA Checker

Project Head Josef Widder:
Parametrized Verification of Fault-tolerant Distributed Algorithms