Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-12002-2_11 | TACAS |
Keywords | Field | DocType |
boolean device driver model,karp-miller tree construction,non-recursive concurrent program,predicate abstraction,boolean program,concurrent version,thread counter,bounded counter,unbounded thread creation,boolean program model,counter abstraction,model checking,programming model,partial order reduction | Abstraction model checking,Model checking,Programming language,Predicate abstraction,Computer science,Reachability,Theoretical computer science,Thread (computing),Partial order reduction,Boom,Bounded function | Conference |
Volume | ISSN | ISBN |
6015 | 0302-9743 | 3-642-12001-6 |
Citations | PageRank | References |
9 | 0.56 | 12 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerard Basler | 1 | 268 | 8.11 |
| Matthew Hague | 2 | 167 | 14.74 |
| Daniel Kroening | 3 | 3084 | 187.60 |
| C.-H. Luke Ong | 4 | 700 | 65.45 |
| Thomas Wahl | 5 | 266 | 11.57 |
| Haoxian Zhao | 6 | 9 | 0.56 |