Boom: Taking Boolean Program Model Checking One Step Further

Abstract. 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.

• Type: Conference
• Year: 2010
• Where: TACAS
• Authors: Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao
• Keywords: Algorithms, Boom, Non-recursive Concurrent Programs, TACAS 2010, Unbounded Thread Creation