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.
|出版ステータス||出版済み - 1 1 2013|
|イベント||2013 International Conference on Computer Sciences and Applications, CSA 2013 - Wuhan, 中国|
継続期間: 12 14 2013 → 12 15 2013
|その他||2013 International Conference on Computer Sciences and Applications, CSA 2013|
|Period||12/14/13 → 12/15/13|
All Science Journal Classification (ASJC) codes
- コンピュータ サイエンスの応用