{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:05Z","timestamp":1772164025616,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T00:00:00Z","timestamp":1498003200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,21]]},"DOI":"10.1145\/3078633.3081035","type":"proceedings-article","created":{"date-parts":[[2017,6,9]],"date-time":"2017-06-09T13:40:22Z","timestamp":1497015622000},"page":"61-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems"],"prefix":"10.1145","author":[{"given":"Min","family":"Zhang","sequence":"first","affiliation":[{"name":"East China Normal Univeristy, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yunhui","family":"Ying","sequence":"additional","affiliation":[{"name":"East China Normal Univeristy, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,6,21]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542452.1542475"},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"590","volume-title":"Proceedings of the 10th TACAS","author":"Bardin S.","unstructured":"S. Bardin , A. Finkel , and J. Leroux . FASTer acceleration of counter automata in practice . In Proceedings of the 10th TACAS , volume 2988 of LNCS , pages 576\u2013 590 . Springer, 2004. S. Bardin, A. Finkel, and J. Leroux. FASTer acceleration of counter automata in practice. In Proceedings of the 10th TACAS, volume 2988 of LNCS, pages 576\u2013590. Springer, 2004."},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","first-page":"177","volume-title":"Proceedings of the 23rd CAV","author":"Barrett C.","unstructured":"C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovi\u00b4c , T. King , A. Reynolds , and C. Tinelli . CVC4 . In Proceedings of the 23rd CAV , volume 6806 of LNCS , pages 171\u2013 177 . Springer, 2011. C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u00b4c, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proceedings of the 23rd CAV, volume 6806 of LNCS, pages 171\u2013177. Springer, 2011."},{"key":"e_1_3_2_1_5_1","volume-title":"The SMT-LIB standard: Version 2.5. SMT-LIB. org","author":"Barrett C.","year":"2016","unstructured":"C. Barrett , P. Fontaine , and C. Tinelli . The SMT-LIB standard: Version 2.5. SMT-LIB. org , 2016 . C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB standard: Version 2.5. SMT-LIB. org, 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29645-1_12"},{"key":"e_1_3_2_1_8_1","first-page":"207","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Cimatti A.","unstructured":"A. Cimatti , M. Pistore , M. Roveri , and R. Sebastiani . Improving the encoding of LTL model checking into SAT . In International Workshop on Verification, Model Checking, and Abstract Interpretation , pages 196\u2013 207 . Springer, 2002. A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani. Improving the encoding of LTL model checking into SAT. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 196\u2013207. Springer, 2002."},{"key":"e_1_3_2_1_9_1","volume-title":"SystemVerilog Assertions Handbook:\u2013for Formal and Dynamic Verification","author":"Cohen B.","year":"2005","unstructured":"B. Cohen , S. Venkataramanan , and A. Kumari . SystemVerilog Assertions Handbook:\u2013for Formal and Dynamic Verification . VhdlCohen Publishing , 2005 . B. Cohen, S. Venkataramanan, and A. Kumari. SystemVerilog Assertions Handbook:\u2013for Formal and Dynamic Verification. VhdlCohen Publishing, 2005."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190109"},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","first-page":"340","volume-title":"Proceedings of the 14th TACAS","author":"de Moura L. M.","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: an efficient SMT solver . In Proceedings of the 14th TACAS , volume 4963 of LNCS , pages 337\u2013 340 . Springer, 2008. L. M. de Moura and N. Bj\u00f8rner. Z3: an efficient SMT solver. In Proceedings of the 14th TACAS, volume 4963 of LNCS, pages 337\u2013 340. Springer, 2008."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_4"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2554850.2554929"},{"key":"e_1_3_2_1_15_1","first-page":"49","volume-title":"Cyber-Physical Systems. In Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems","author":"Mallet F.","unstructured":"F. Mallet . MARTE\/ CCSL for modeling Cyber-Physical Systems. In Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems , pages 26\u2013 49 . Springer, 2015. F. Mallet. MARTE\/CCSL for modeling Cyber-Physical Systems. In Proceedings of the Formal Modeling and Verification of Cyber-Physical Systems, pages 26\u201349. Springer, 2015."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.03.001"},{"key":"e_1_3_2_1_17_1","volume-title":"UML profile for MARTE: modeling and analysis of real-time embedded systems","author":"OMG.","year":"2015","unstructured":"OMG. UML profile for MARTE: modeling and analysis of real-time embedded systems , 2015 . OMG. UML profile for MARTE: modeling and analysis of real-time embedded systems, 2015."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40561-7_1"},{"key":"e_1_3_2_1_19_1","first-page":"231","volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe","author":"Vidal J.","unstructured":"J. Vidal , F. De Lamotte , G. Gogniat , P. Soulard , and J.-P. Diguet . A codesign approach for embedded system modeling and code generation with UML and MARTE . In Proceedings of the Conference on Design, Automation and Test in Europe , pages 226\u2013 231 . European Design and Automation Association, 2009. J. Vidal, F. De Lamotte, G. Gogniat, P. Soulard, and J.-P. Diguet. A codesign approach for embedded system modeling and code generation with UML and MARTE. In Proceedings of the Conference on Design, Automation and Test in Europe, pages 226\u2013231. European Design and Automation Association, 2009."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2011.14"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970507"},{"key":"e_1_3_2_1_22_1","series-title":"CCIS","first-page":"51","volume-title":"Proceedings of the 4th FTSCS","author":"Zhang M.","unstructured":"M. Zhang and F. Mallet . An executable semantics of clock constraint specification language and its applications . In Proceedings of the 4th FTSCS , volume 596 of CCIS , pages 37\u2013 51 . Springer, 2015. M. Zhang and F. Mallet. An executable semantics of clock constraint specification language and its applications. In Proceedings of the 4th FTSCS, volume 596 of CCIS, pages 37\u201351. Springer, 2015."},{"key":"e_1_3_2_1_23_1","series-title":"LNCS","first-page":"449","volume-title":"Proceedings of the 18th ICFEM","author":"Zhang M.","unstructured":"M. Zhang , F. Mallet , and H. Zhu . An SMT-based approach to the formal analysis of MARTE\/CCSL . In Proceedings of the 18th ICFEM , volume 10009 of LNCS , pages 433\u2013 449 . Springer, 2016. M. Zhang, F. Mallet, and H. Zhu. An SMT-based approach to the formal analysis of MARTE\/CCSL. In Proceedings of the 18th ICFEM, volume 10009 of LNCS, pages 433\u2013449. Springer, 2016."},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","first-page":"292","volume-title":"Proceedings of FMICS","author":"Zhang W.","year":"2006","unstructured":"W. Zhang . SAT-based verification of LTL formulas . In Proceedings of FMICS 2006 , volume 4346 of LNCS , pages 277\u2013 292 . Springer, 2006. W. Zhang. SAT-based verification of LTL formulas. In Proceedings of FMICS 2006, volume 4346 of LNCS, pages 277\u2013292. Springer, 2006."}],"event":{"name":"LCTES '17: SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2017","location":"Barcelona Spain","acronym":"LCTES '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 18th ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3078633.3081035","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3078633.3081035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:30:31Z","timestamp":1750203031000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3078633.3081035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,21]]},"references-count":23,"alternative-id":["10.1145\/3078633.3081035","10.1145\/3078633"],"URL":"https:\/\/doi.org\/10.1145\/3078633.3081035","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3140582.3081035","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,6,21]]},"assertion":[{"value":"2017-06-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}