A Comparison of SAT-Based and SMT-Based Bounded Model Checking Methods for ECTL.
Agnieszka M. Zbrzezny, Andrzej Zbrzezny · CS&P · 2014
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 semantics 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 experimental 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.