## Exploiting replication in automated program verification

##### Abstract

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.