A survey of acceleration techniques for SMT-based bounded model checking

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

研究成果: Contribution to conferencePaper査読

3 被引用数 (Scopus)

抄録

Model checking is wildly acknowledged to be an effective formal technique for verifying that a finite state system satisfies desired properties expressed in temporal logic. There are primarily two types of model checking approaches: explicit model checking and symbolic model checking. To mitigate the notorious state exploration problems suffered by explicit model checking, bounded model checking (BMC) has been proposed as an alternative to other symbolic model checking approaches based on binary decision diagrams. Although originally SAT solvers are used by BMC as the reasoning engine, a recent trend is to switch from SAT to SMT solvers. In this paper, we survey contributions on acceleration of SMT-based BMC. In addition, we discuss some related techniques that could be potentially used as well for the acceleration purpose.

本文言語英語
ページ554-559
ページ数6
DOI
出版ステータス出版済み - 1 1 2013
イベント2013 International Conference on Computer Sciences and Applications, CSA 2013 - Wuhan, 中国
継続期間: 12 14 201312 15 2013

その他

その他2013 International Conference on Computer Sciences and Applications, CSA 2013
国/地域中国
CityWuhan
Period12/14/1312/15/13

All Science Journal Classification (ASJC) codes

  • コンピュータ サイエンスの応用

フィンガープリント

「A survey of acceleration techniques for SMT-based bounded model checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル