{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:10Z","timestamp":1750308550203,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,11,11]],"date-time":"2014-11-11T00:00:00Z","timestamp":1415664000000},"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":[[2014,11,11]]},"DOI":"10.1145\/2635868.2635911","type":"proceedings-article","created":{"date-parts":[[2014,11,4]],"date-time":"2014-11-04T21:44:36Z","timestamp":1415137476000},"page":"213-223","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying CTL-live properties of infinite state models using an SMT solver"],"prefix":"10.1145","author":[{"given":"Amirhossein","family":"Vakili","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]}],"member":"320","published-online":{"date-parts":[[2014,11,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Python. http:\/\/www.python.org.  Python. http:\/\/www.python.org."},{"key":"e_1_3_2_1_2_1","volume-title":"Concurrent Programming: Principles and Practice","author":"Andrews G. R.","year":"1991","unstructured":"G. R. Andrews . Concurrent Programming: Principles and Practice . Benjamin-Cummings Publishing Co., Inc. , 1991 . G. R. Andrews. Concurrent Programming: Principles and Practice. Benjamin-Cummings Publishing Co., Inc., 1991."},{"key":"e_1_3_2_1_3_1","unstructured":"C.\n      Barrett R.\n      Sebastiani S.\n      Seshia and \n      C.\n      Tinelli\n  . \n  Satisfiability Modulo Theories volume \n  185\n   of \n  Frontiers in Artificial Intelligence and Applications chapter 26 pages 825\u2013\n  885\n  . IOS Press February 2009.  C. Barrett R. Sebastiani S. Seshia and C. Tinelli. Satisfiability Modulo Theories volume 185 of Frontiers in Artificial Intelligence and Applications chapter 26 pages 825\u2013885. IOS Press February 2009."},{"key":"e_1_3_2_1_4_1","volume-title":"Jan.","author":"Barrett C.","year":"2010","unstructured":"C. Barrett , A. Stump , and C. Tinelli . The SMT-LIB Standard Version 2.0 Reference Manual , Jan. 2010 . C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard Version 2.0 Reference Manual, Jan. 2010."},{"key":"e_1_3_2_1_5_1","first-page":"302","volume-title":"CAV","author":"Barrett C.","unstructured":"C. Barrett and C. Tinelli . CVC3 . In CAV , pages 298\u2013 302 . Springer-Verlag, 2007. C. Barrett and C. Tinelli. CVC3. In CAV, pages 298\u2013302. Springer-Verlag, 2007."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958062"},{"key":"e_1_3_2_1_7_1","first-page":"193","volume":"1579","author":"Biere A.","year":"1999","unstructured":"A. Biere , A. Cimatti , E. Clarke , and Y. Zhu . Symbolic Model Checking without BDDs. In TACAS , volume 1579 of LNCS, pages 193 \u2013 207 . Springer, 1999 . A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. In TACAS, volume 1579 of LNCS, pages 193\u2013207. Springer, 1999.","journal-title":"Symbolic Model Checking without BDDs. In TACAS"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"87","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Bradley A.","unstructured":"A. Bradley . SAT-Based Model Checking without Unrolling . In Verification, Model Checking, and Abstract Interpretation , volume 6538 of LNCS , pages 70\u2013 87 . Springer Berlin Heidelberg, 2011. A. Bradley. SAT-Based Model Checking without Unrolling. In Verification, Model Checking, and Abstract Interpretation, volume 6538 of LNCS, pages 70\u201387. Springer Berlin Heidelberg, 2011."},{"key":"e_1_3_2_1_9_1","first-page":"400","volume":"1254","author":"Bultan T.","year":"1997","unstructured":"T. Bultan , R. Gerber , and W. Pugh . Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. In CAV , volume 1254 of LNCS, pages 400 \u2013 411 . Springer, 1997 . T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. In CAV, volume 1254 of LNCS, pages 400\u2013411. Springer, 1997.","journal-title":"In CAV"},{"key":"e_1_3_2_1_10_1","volume-title":"Feb.","author":"Cavada R.","year":"2014","unstructured":"R. Cavada , A. Cimatti , M. Dorigatti , A. Mariotti , A. Micheli , S. Mover , A. Griggio , M. Roveri , and S. Tonetta . The nuXmv Symbolic Model Checker. Technical report , Feb. 2014 . R. Cavada, A. Cimatti, M. Dorigatti, A. Mariotti, A. Micheli, S. Mover, A. Griggio, M. Roveri, and S. Tonetta. The nuXmv Symbolic Model Checker. Technical report, Feb. 2014."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_1_13_1","volume-title":"IC3 modulo theories via implicit predicate abstraction. CoRR, abs\/1310.6847","author":"Cimatti A.","year":"2013","unstructured":"A. Cimatti , A. Griggio , S. Mover , and S. Tonetta . IC3 modulo theories via implicit predicate abstraction. CoRR, abs\/1310.6847 , 2013 . A. Cimatti, A. Griggio, S. Mover, and S. Tonetta. IC3 modulo theories via implicit predicate abstraction. CoRR, abs\/1310.6847, 2013."},{"key":"e_1_3_2_1_14_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. A. Peled . Model Checking . MIT Press , 1999 . E. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_1_17_1","first-page":"337","volume":"4963","author":"de Moura L.","year":"2008","unstructured":"L. de Moura and N. Bj\u00f8rner . Z3: An Efficient SMT Solver. In TACAS , volume 4963 of LNCS, pages 337 \u2013 340 . Springer, 2008 . L. de Moura and N. Bj\u00f8rner. Z3: An Efficient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer, 2008.","journal-title":"Z3: An Efficient SMT Solver. In TACAS"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/975331"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_21_1","unstructured":"D. Jackson. Software Abstractions - Logic Language and Analysis. MIT Press 2006.   D. Jackson. Software Abstractions - Logic Language and Analysis. MIT Press 2006."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.023"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232743.1232745"},{"key":"e_1_3_2_1_25_1","first-page":"237","volume-title":"LNCS","author":"McMillan K.","unstructured":"K. McMillan . Verification of infinite state systems by compositional model checking. In Correct Hardware Design and Verification Methods , LNCS , pages 219\u2013 237 . Springer Berlin Heidelberg, 1999. K. McMillan. Verification of infinite state systems by compositional model checking. In Correct Hardware Design and Verification Methods, LNCS, pages 219\u2013237. Springer Berlin Heidelberg, 1999."},{"key":"e_1_3_2_1_26_1","volume-title":"Nov. 06","author":"McMillan K. L.","year":"1992","unstructured":"K. L. McMillan . The SMV system , Nov. 06 1992 . K. L. McMillan. The SMV system, Nov. 06 1992."},{"key":"e_1_3_2_1_27_1","first-page":"81","volume-title":"Formal Methods in System Design","author":"Sch\u00fcle T.","year":"2007","unstructured":"T. Sch\u00fcle and K. Schneider . Bounded model checking of infinite state systems . Formal Methods in System Design , pages 51\u2013 81 , 2007 . T. Sch\u00fcle and K. Schneider. Bounded model checking of infinite state systems. Formal Methods in System Design, pages 51\u201381, 2007."},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"144","volume-title":"FMCAD","author":"Sheeran M.","unstructured":"M. Sheeran , S. Singh , and G. St\u02da almarck. Checking Safety Properties Using Induction and a SAT-Solver . In FMCAD , volume 1954 of LNCS , pages 127\u2013 144 . Springer, 2000. M. Sheeran, S. Singh, and G. St\u02da almarck. Checking Safety Properties Using Induction and a SAT-Solver. In FMCAD, volume 1954 of LNCS, pages 127\u2013144. Springer, 2000."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2664431.2664437"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682960"},{"key":"e_1_3_2_1_32_1","volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock J.","year":"1996","unstructured":"J. Woodcock and J. Davies . Using Z: Specification, Refinement, and Proof . Prentice-Hall, Inc. , 1996 . J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., 1996."}],"event":{"name":"SIGSOFT\/FSE'14: 22nd ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Hong Kong China","acronym":"SIGSOFT\/FSE'14"},"container-title":["Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2635868.2635911","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2635868.2635911","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:44Z","timestamp":1750273424000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2635868.2635911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,11]]},"references-count":29,"alternative-id":["10.1145\/2635868.2635911","10.1145\/2635868"],"URL":"https:\/\/doi.org\/10.1145\/2635868.2635911","relation":{},"subject":[],"published":{"date-parts":[[2014,11,11]]},"assertion":[{"value":"2014-11-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}