Exploiting replication in automated program verification

This dissertation shows how systems of many concurrent components, which naively engender intractably large state spaces, can nevertheless be successfully subject to exhaustive formal verification, provided the components can be classified into a few types. It therefore addresses an instance of the state explosion problem: a finite-state model of a system can be much larger than a high-level description of this system. Model checking, the technique to which this dissertation is primarily devoted, inherently relies on state space exploration and thus suffers from this problem more than other formal verification methods. The state explosion phenomenon persists even if the system consists of components that are simply replicated instances of a generic behavioral description. Examples of such systems abound; they include processes executing concurrently according to some common protocol, clusters of processors executing a parallel provii gram, and hardware with replicated physical devices in a uniform arrangement. Fortunately, models of such systems often exhibit a regular structure, known as symmetry, which can be exploited in verification, sometimes to the extent of an exponential reduction in model size. The first contribution of this dissertation is to show how reductions based on symmetry can be performed with state-of-the-art system representations. Many of today’s computing systems induce astronomically large state spaces whose formal models require a symbolic encoding using boolean formulas. Such succinct representations call for new algorithms that can process entire sets of objects at once. How to detect symmetry quickly during symbolic model checking, so that redundancy in the exploration can be avoided, was an open problem for some time. In this dissertation we provide an efficient and flexible solution to this problem by using symbolic data structures in a somewhat unconventional way. The second contribution is to extend symmetry reduction techniques to more realistic and general scenarios. We establish that the principal ideas still apply if symmetry is violated in parts of the state space. Such scenarios are common in practice, for instance when priorities determine which of several competing processes can access a resource first. In these situations it is beneficial to exploit symmetry where it exists and watch out for the (few) violations, rather than to ignore it altogether. We also demonstrate how symmetry can help us solve a practically significant instance of parameterized verification of system families. This technique traditionally attempts to prove properties about systems independently of the size parameter, but requires models of a special structure. We show that by restricting the parameter to a finite range we can solve this problem efficiently, can do so without any conditions on the models’ structure, and can take advantage of symmetry in the individual systems of the family if it exists.