Harnessing SMT-based bounded model checking through stateless explicit-state exploration

Weiqiang Kong, Leyuan Liu, Takahiro Ando, Hirokazu Yatsu, Kenji Hisazumi, Akira Fukuda

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

2 引用 (Scopus)

抜粋

We propose a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicitstate exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing, together with the encoded formula for an LTL property, independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2 with CVC4 as its backend solver. The experimental results show that Garakabu2 often outperforms the state-of-the-art pure BMC methods implemented in SAL infinite bounded model checker for both safety and liveness properties.

元の言語英語
ホスト出版物のタイトルAPSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference
編集者Pornsiri Muenchaisri, Gregg Rothermel
出版者IEEE Computer Society
ページ355-362
ページ数8
ISBN(電子版)9781479921430
ISBN(印刷物)9780769549224
DOI
出版物ステータス出版済み - 1 1 2013
イベント20th Asia-Pacific Software Engineering Conference, APSEC 2013 - Bangkok, タイ
継続期間: 12 2 201312 5 2013

出版物シリーズ

名前Proceedings - Asia-Pacific Software Engineering Conference, APSEC
1
ISSN(印刷物)1530-1362

その他

その他20th Asia-Pacific Software Engineering Conference, APSEC 2013
タイ
Bangkok
期間12/2/1312/5/13

All Science Journal Classification (ASJC) codes

  • Software

フィンガープリント Harnessing SMT-based bounded model checking through stateless explicit-state exploration' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Kong, W., Liu, L., Ando, T., Yatsu, H., Hisazumi, K., & Fukuda, A. (2013). Harnessing SMT-based bounded model checking through stateless explicit-state exploration. : P. Muenchaisri, & G. Rothermel (版), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference (pp. 355-362). [6805426] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; 巻数 1). IEEE Computer Society. https://doi.org/10.1109/APSEC.2013.55