论文标题
分布式有限模型检查
Distributed Bounded Model Checking
论文作者
论文摘要
程序验证是一项渴望资源的任务。本文着眼于并行化基于SMT的自动化程序验证的问题，特别是有界模型检查，以便可以在一组机器上分发和执行。我们提出了一种动态展开程序的呼叫图并经常将其拆分以创建可以并行解决的子任务的算法。该算法是自适应的，根据可用资源控制分裂速率，还利用SMT求解器的信息到搜索中最复杂的地方分开。我们通过修改Corral（Microsoft的静态驱动程序验证仪（SDV）使用的验证者）实现了算法，并在一系列硬式SDV基准测试中对其进行了评估。
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.
