Monotonic Abstraction in Parameterized Verification

We present a tutorial on verification of safety properties for parameterized systems. Such a system consists of an arbitrary number of processes which are organized in a linear array. The aim is to prove correctness of the system regardless of the number of processes inside the system. We give an overview of the method of monotonic abstraction, which provides an over-approximation of the transition system induced by a parameterized system. The over-approximation gives a transition system which is monotonic with respect to a well quasi-ordering on the set of configurations. This makes it possible to use existing methods for verification of well quasi-ordered programs.