Boom: Taking Boolean Program Model Checking One Step Further
Boom: Taking Boolean Program Model Checking One Step Further
复制标题
Boom：布尔程序模型检查更进一步
DOI：
10.1007/978-3-642-12002-2_11
复制
发表时间：
2010
影响因子：
0.8
通讯作者：
Haoxian Zhao
中科院分区：
文献类型：
--
作者：
Gérard Basler;M. Hague;D. Kroening;C. Ong;T. Wahl;Haoxian Zhao
我们提出BOOM，这是布尔计划的综合分析工具。我们在本文中重点介绍了模型检查非恢复并发程序。 Boom实现了最新的反抽象变体，其中线程计数器以程序上下文意识的方式使用。虽然为有界计数器设计，但此方法还与用于矢量添加系统的KARP-MILLER树的构造良好，从而为具有无限线程创建的程序提供了可及性引擎。 Boom的并发版本使用BDD实现，并包括部分订单减少方法。 Boom旨在通过谓词抽象来模型检查系统级代码。我们提出了验证布尔设备驱动器模型的实验结果。
We present Boom, a comprehensive analysis tool for Boolean programs. We focus in this paper on model-checking non-recursive concurrent programs. Boom implements a recent variant of counter abstraction, where thread counters are used in a program-context aware way. While designed for bounded counters, this method also integrates well with the Karp-Miller tree construction for vector addition systems, resulting in a reachability engine for programs with unbounded thread creation. The concurrent version of Boom is implemented using BDDs and includes partial order reduction methods. Boom is intended for model checking system-level code via predicate abstraction. We present experimental results for the verification of Boolean device driver models.