{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:13:14Z","timestamp":1760202794623,"version":"3.28.0"},"reference-count":39,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603008","type":"proceedings-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T20:33:52Z","timestamp":1546979632000},"page":"1-11","source":"Crossref","is-referenced-by-count":7,"title":["Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems"],"prefix":"10.23919","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref39","DOI":"10.1016\/j.cl.2015.10.001"},{"doi-asserted-by":"publisher","key":"ref38","DOI":"10.1007\/978-3-319-10936-7_19"},{"doi-asserted-by":"publisher","key":"ref33","DOI":"10.1109\/LICS.2004.1319598"},{"doi-asserted-by":"publisher","key":"ref32","DOI":"10.1007\/10722167_26"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1145\/2908080.2908118","article-title":"Ivy: safety verification by interactive generalization","author":"padon","year":"2016","journal-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2016"},{"key":"ref30","first-page":"26:1","article-title":"Reducing liveness to safety in first-order logic","volume":"2","author":"padon","year":"2018","journal-title":"PACMPL"},{"doi-asserted-by":"publisher","key":"ref37","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"ref36","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-662-49674-9_4","article-title":"Synthesizing ranking functions from bits and pieces","volume":"9636","author":"urban","year":"2016","journal-title":"TACAS Ser Lecture Notes in Computer Science"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","article-title":"The abstract domain of segmented ranking functions","volume":"7935","author":"urban","year":"2013","journal-title":"SAS Ser Lecture Notes in Computer Science"},{"doi-asserted-by":"publisher","key":"ref34","DOI":"10.1145\/1040305.1040317"},{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1145\/1926385.1926431"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1145\/1941487.1941509"},{"doi-asserted-by":"publisher","key":"ref12","DOI":"10.1007\/978-3-642-36742-7_4"},{"year":"2008","author":"corbet","article-title":"Ticket spinlocks","key":"ref13"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1145\/2103656.2103687"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","article-title":"Fairness modulo theory: A new approach to LTL software model checking","volume":"9206","author":"dietsch","year":"2015","journal-title":"CAV Ser Lecture Notes in Computer Science"},{"doi-asserted-by":"publisher","key":"ref16","DOI":"10.1007\/11888116_26"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/2933575.2935310","article-title":"Proving liveness of param-eterized programs","author":"farzan","year":"2016","journal-title":"LICS ACM"},{"key":"ref18","first-page":"397","article-title":"Proving termination starting from the end","author":"ganty","year":"2013","journal-title":"2013 Proceedings"},{"key":"ref19","first-page":"306","article-title":"Complete instantiation for quantified formulas in satisfiabiliby modulo theories","author":"ge","year":"2009","journal-title":"International Conference on Computer Aided Verification"},{"doi-asserted-by":"publisher","key":"ref28","DOI":"10.1007\/978-3-319-41528-4_23"},{"doi-asserted-by":"publisher","key":"ref4","DOI":"10.1109\/SEFM.2007.32"},{"doi-asserted-by":"publisher","key":"ref27","DOI":"10.1007\/978-3-642-31424-7_12"},{"doi-asserted-by":"publisher","key":"ref3","DOI":"10.1007\/11817949_7"},{"doi-asserted-by":"publisher","key":"ref6","DOI":"10.1145\/70082.68193"},{"doi-asserted-by":"publisher","key":"ref29","DOI":"10.1016\/S0167-6423(99)00030-1"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1016\/S1571-0661(04)80410-9"},{"doi-asserted-by":"publisher","key":"ref8","DOI":"10.1145\/1133981.1134029"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1007\/978-3-642-39799-8_28"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-3-319-21690-4_2","article-title":"On automation of ctl* verification for infinite-state systems","volume":"9206","author":"cook","year":"2015","journal-title":"Proceedings Part I-III Ser Lecture Notes in Computer Science"},{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1016\/0304-3975(89)90138-2"},{"doi-asserted-by":"publisher","key":"ref20","DOI":"10.1007\/978-3-540-25979-4_15"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.1145\/1542476.1542518"},{"doi-asserted-by":"publisher","key":"ref21","DOI":"10.1145\/2254064.2254112"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","article-title":"Termination analysis by learning terminating programs","volume":"8559","author":"heizmann","year":"2014","journal-title":"CAV Ser Lecture Notes in Computer Science"},{"doi-asserted-by":"publisher","key":"ref23","DOI":"10.1007\/978-3-642-15769-1_19"},{"doi-asserted-by":"publisher","key":"ref26","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"ref25","first-page":"101","article-title":"Network invariants in action","author":"kesten","year":"0"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2018,10,30]]},"location":"Austin, TX","end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603008.pdf?arnumber=8603008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,25]],"date-time":"2022-01-25T18:51:30Z","timestamp":1643136690000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603008\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":39,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603008","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}