{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T17:01:18Z","timestamp":1768323678693,"version":"3.49.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987598","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"75-82","source":"Crossref","is-referenced-by-count":7,"title":["Faster temporal reasoning for infinite-state programs"],"prefix":"10.1109","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heidy","family":"Khlaaf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","DOI":"10.1007\/10720246_1","article-title":"Planning as model checking","author":"giunchiglia","year":"2000","journal-title":"Recent advances in AI planning"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"18","doi-asserted-by":"crossref","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meaning to programs","author":"floyd","year":"1967","journal-title":"Mathematical Aspects of Computer Science Ser Proc of Symposia in Applied Mathematics"},{"key":"33","article-title":"Pushdown processes: Games and model checking","volume":"96","author":"walukiewicz","year":"1996","journal-title":"CAV"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386390"},{"key":"34","article-title":"Model checking ctl properties of pushdown systems","author":"walukiewicz","year":"2000","journal-title":"FSTTCS'00"},{"key":"16","article-title":"Automatic verification of parameterized synchronous systems (extended abstract","volume":"96","author":"emerson","year":"1996","journal-title":"CAV"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926431"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_11"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"20","doi-asserted-by":"crossref","DOI":"10.1145\/1480881.1480886","article-title":"Proving that non-blocking algorithms don't block","volume":"9","author":"gotsman","year":"2009","journal-title":"POPL"},{"key":"22","article-title":"Yasm: A software modelchecker for verification and refutation","volume":"6","author":"gurfinkel","year":"2006","journal-title":"CAV"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_22"},{"key":"24","doi-asserted-by":"crossref","DOI":"10.1016\/j.tcs.2004.09.023","article-title":"A compositional approach to ctl verification","volume":"331","author":"kesten","year":"2005","journal-title":"Theor Comput Sci"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_26"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"28","article-title":"Lazy abstraction with interpolants","author":"mcmillan","year":"2006","journal-title":"CAV"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2002.1106750"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_50"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491969"},{"key":"1","year":"0","journal-title":"T2 Source Code"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029814"},{"key":"6","article-title":"Nusmv 2: An opensource tool for symbolic model checking","volume":"2","author":"cimatti","year":"2002","journal-title":"CAV"},{"key":"32","article-title":"Pushdown model checking for malware detection","volume":"12","author":"song","year":"2012","journal-title":"TACAS"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"9","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"1981","journal-title":"Proc Workshop on Logic of Programs"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,21]]},"end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987598.pdf?arnumber=6987598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T06:57:12Z","timestamp":1690786632000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987598\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987598","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}