Distributed Bounded Model Checking

Program verification is a resource-hungry task. This
paper looks at the problem of parallelizing SMT-based automated
program verification, specifically bounded model-checking, so
that it can be distributed and executed on a cluster of machines.
We present an algorithm that dynamically unfolds the call graph
of the program and frequently splits it to create sub-tasks that can
be solved in parallel. The algorithm is adaptive, controlling the
splitting rate according to available resources, and also leverages
information from the SMT solver to split where most complexity
lies in the search. We implemented our algorithm by modifying
CORRAL, the verifier used by Microsoft’s Static Driver Verifier
(SDV), and evaluate it on a series of hard SDV benchmarks.