TY - JOUR
KW - RTECTL
KW - STS
KW - SMT
AU - Agnieszka Zbrzezny
AU - Andrzej Zbrzezny
AB - We present an SMT-based bounded model checking (BMC) method for Simply-Timed Systems (STSs) and for the existential fragment of the Real-time Computation Tree Logic. We implemented the SMT-based BMC algorithm and compared it with the SAT-based BMC method for the same systems and the same property language on several benchmarks for STSs. For the SAT- based BMC we used the PicoSAT solver and for the SMT-based BMC we used the Z3 solver. The experimental results show that the SMT-based BMC performs quite well and is, in fact, sometimes significantly faster than the tested SAT-based BMC.
IS - Regular Issue
M1 - 5
N2 - We present an SMT-based bounded model checking (BMC) method for Simply-Timed Systems (STSs) and for the existential fragment of the Real-time Computation Tree Logic. We implemented the SMT-based BMC algorithm and compared it with the SAT-based BMC method for the same systems and the same property language on several benchmarks for STSs. For the SAT- based BMC we used the PicoSAT solver and for the SMT-based BMC we used the Z3 solver. The experimental results show that the SMT-based BMC performs quite well and is, in fact, sometimes significantly faster than the tested SAT-based BMC.
PY - 2015
SP - 28
EP - 35
T2 - International Journal of Interactive Multimedia and Artificial Intelligence
TI - Checking RTECTL properties of STSs via SMT-based Bounded Model Checking
UR - http://www.ijimai.org/journal/sites/default/files/files/2015/11/ijimai20153_5_4_pdf_87485.pdf
VL - 3
SN - 1989-1660
ER -