  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.
