Boom: Model Checking for Asynchronous Boolean Programs

Boolean programs have gained importance as a representation of abstract models that are automatically generated from high-level programs by the widely-used predicate abstraction-refinement framework. The underlaying (reachability) analysis remains the bottleneck of this approach.

In the first part of the talk we will present how we improved existing methods for the reachability analysis of recursive sequential Boolean programs. The second part describes a novel variant of the Karp-Miller tree construction that permits reachability analysis of non-recursive concurrent Boolean programs with unbounded thread creation. The algorithms are implemented in Boom, a model checking platform for Boolean programs. It is the first tool that implements a summarizing reachability engine that entirely relies on a SAT/QBF solver. The concurrent variant of Boom is implemented using BDDs and includes partial order reduction methods. Furthermore, we present extensive experimental results for the verification of Boolean device driver models.