Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. - Min Zhang 002; Yunhui Ying (LCTES, 2017)