Distributed Bounded Model Checking

TL;DR

This paper introduces a dynamic, adaptive algorithm for distributed bounded model checking that effectively splits verification tasks across multiple machines, improving efficiency in resource-intensive program verification.

Contribution

It presents a novel adaptive algorithm for parallelizing SMT-based bounded model checking, integrated into CORRAL, enabling scalable distributed verification.

Findings

Effective parallelization of bounded model checking

Improved verification speed on SDV benchmarks

Adaptive splitting based on resource availability

Abstract

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.