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...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2010
|
| _version_ | 1826271571302416384 |
|---|---|
| author | Basler, G Hague, M Kroening, D Ong, C Wahl, T Zhao, H |
| author2 | Esparza, J |
| author_facet | Esparza, J Basler, G Hague, M Kroening, D Ong, C Wahl, T Zhao, H |
| author_sort | Basler, G |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T21:58:45Z |
| format | Conference item |
| id | oxford-uuid:4ddaf658-895a-4d54-bc92-8974c0e98010 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T21:58:45Z |
| publishDate | 2010 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:4ddaf658-895a-4d54-bc92-8974c0e980102022-03-26T15:57:49ZBOOM: Taking Boolean program model checking one step furtherConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4ddaf658-895a-4d54-bc92-8974c0e98010Symplectic Elements at OxfordSpringer2010Basler, GHague, MKroening, DOng, CWahl, TZhao, HEsparza, JMajumdar, RWe 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. |
| spellingShingle | Basler, G Hague, M Kroening, D Ong, C Wahl, T Zhao, H BOOM: Taking Boolean program model checking one step further |
| title | BOOM: Taking Boolean program model checking one step further |
| title_full | BOOM: Taking Boolean program model checking one step further |
| title_fullStr | BOOM: Taking Boolean program model checking one step further |
| title_full_unstemmed | BOOM: Taking Boolean program model checking one step further |
| title_short | BOOM: Taking Boolean program model checking one step further |
| title_sort | boom taking boolean program model checking one step further |
| work_keys_str_mv | AT baslerg boomtakingbooleanprogrammodelcheckingonestepfurther AT haguem boomtakingbooleanprogrammodelcheckingonestepfurther AT kroeningd boomtakingbooleanprogrammodelcheckingonestepfurther AT ongc boomtakingbooleanprogrammodelcheckingonestepfurther AT wahlt boomtakingbooleanprogrammodelcheckingonestepfurther AT zhaoh boomtakingbooleanprogrammodelcheckingonestepfurther |