Distributed Bounded Model Checking
This addresses the computational bottleneck in automated program verification for developers and verification engineers, though it is an incremental improvement to existing methods.
The paper tackles the resource-intensive problem of program verification by parallelizing SMT-based bounded model-checking for distributed execution on clusters, resulting in improved scalability on hard benchmarks from Microsoft's Static Driver Verifier.
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.