@article{2511,
  keywords = {RTECTL, STS, SMT},
  author = {Agnieszka Zbrzezny and Andrzej Zbrzezny},
  title = {Checking RTECTL properties of STSs via SMT-based Bounded Model Checking},
  abstract = {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.},
  year = {2015},
  journal = {International Journal of Interactive Multimedia and Artificial Intelligence},
  volume = {3},
  number = {5},
  pages = {28-35},
  month = {12/2015},
  issn = {1989-1660},
  url = {http://www.ijimai.org/journal/sites/default/files/files/2015/11/ijimai20153_5_4_pdf_87485.pdf},
  doi = {10.9781/ijimai.2015.354},
}