Efficient Large-Scale Model Checking

Abstract

Model checking is a popular technique to systematically and automatically verify system properties.
Unfortunately, the well-known state explosion problem often limits the extent to which it can
be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with
mixed results. We examine one well-known distributed model checker in detail, and show how
a number of additional optimizations in its runtime system enable it to efficiently check very demanding
problem instances on a large-scale, multi-core compute cluster. We analyze the impact of
the distributed algorithms employed, the problem instance characteristics and network overhead.
Finally, we show that the model checker can even obtain good performance in a high-bandwidth
computational grid environment.