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

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

Research output: Contribution to conferencePaperpeer-review

3 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages554-559
Number of pages6
DOIs
Publication statusPublished - Jan 1 2013
Event2013 International Conference on Computer Sciences and Applications, CSA 2013 - Wuhan, China
Duration: Dec 14 2013Dec 15 2013

Other

Other2013 International Conference on Computer Sciences and Applications, CSA 2013
CountryChina
CityWuhan
Period12/14/1312/15/13

All Science Journal Classification (ASJC) codes

  • Computer Science Applications

Fingerprint Dive into the research topics of 'A survey of acceleration techniques for SMT-based bounded model checking'. Together they form a unique fingerprint.

Cite this