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

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.