A comparison of SAT-based and SMT-based bounded model checking methods for ECTL* Extended Abstract???

Abstract. In this paper we present a comparison of the SAT-based bounded model checking (BMC) and SMT-based bounded model checking methods for ECTL * properties of a parallel composition of transition systems. In the both methods we use the parallel composition (of the transition systems) based on the interleaved semantics. Moreover, the both methods use the same bounded se-mantics of ECTL * formulae, the compatible encodings of the transition systems and the compatible translations of ECTL * formulae. For the SAT-based BMC we have used the PicoSAT solver and for the SAT-based BMC we have used the Z3 solver. We have implemented the both methods and made some preliminary ex-perimental results which shows that generally the SAT-based method is superior to the SMT-based method. However, in some cases the SMT-method overcomes the SAT-based method.