Model checking is an algorithmic method for verifying correctness of
finite state systems that originated as part of the speaker's dissertation
work. Now, twenty years later, it is widely used in the computer hardware
industry to formally verify and debug microprocessor designs, and
is showing promise for software verification.
The chief limitation to the more widespread
application of model checking is the state explosion problem,
where the size of the system's global state graph grows exponentially with the
number of subprocesses running concurrently in the system. This talk will
examine various strategies for ameliorating state explosion. Some of
these depend on exploiting the symmetry inherent in systems composed of
many (nearly) homogeneous processes. Exponential savings are often possible.
Others permit model checking an infinite family of uniformly parameterized
systems (e.g., token rings of size n, for all n) in one fell swoop.
