Boom: Taking Boolean program model checking one step further 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
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Basler, Gérard; Donaldson, Alastair; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas: satAbs: a bit-precise verifier for C programs. (Competition contribution) (2012)
- Basler, Gerard; Hague, Matthew; Kroening, Daniel; Ong, C.-H.Luke; Wahl, Thomas; Zhao, Haoxian: Boom: taking Boolean program model checking one step further (2010)