Implication-based approximating bounded model checking
Zhenyu Chen, Zhi-Hong Tao, Baowen Xu, Lifu Wang · 2007
Abstract. This paper presents an iterative framework based on over-approximation and under-approximation for traditional bounded model checking (BMC). A novel feature of our approach is the approximations are defined based on “implication ” instead of “simulation”. As a com-mon partial order relation of logic formulas, implication is suitable for the satisfiability checking of BMC for debugging. Our approach could generate the implication-based approximations efficiently with necessary accuracy, thus it potentially enables BMC to go deeper and the output counterexamples with fewer variables are easier to understand. An exper-iment on a suite of Petri nets shows the effectiveness of implication-based approximating BMC.