CMI Silver Jubilee Lecture
Parosh Aziz Abdulla, Uppsala University, Sweden
Cut-offs in Parameterized Verification
Wednesday, December 10, 2014
The "parameterized verification problem" is to prove or refute that some specification is true for all values of the parameters. The parameters may relate to the size or topology of a network, to data types over which a system is constructed, to initial values of variables, etc.
There is strong empirical evidence that many classes of parameterized systems often enjoy a small model property, in the sense thatnanalyzing only a small number of processes (rather than the whole family) is sufficient to capture the reachability of bad configurations.
We introduce a method that exploits the small model property, and performs parameterized verification by only inspecting a small set of fixed instances of the system. The method relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue.
Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. Such systems include mutual exclusion protocols, cache coherence protocols, concurrent data structures, and programs operating on unbounded structures such as stacks and queues.