{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T22:11:11Z","timestamp":1729635071085,"version":"3.28.0"},"reference-count":14,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987616","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"215-218","source":"Crossref","is-referenced-by-count":2,"title":["Reducing CTL-live model checking to first-order logic validity checking"],"prefix":"10.1109","author":[{"given":"Amirhossein","family":"Vakili","sequence":"first","affiliation":[]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"13","first-page":"869","article-title":"Solving existentially quantified horn clauses ser","author":"beyene","year":"2013","journal-title":"CAV"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635911"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"12","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","article-title":"A compositional approach to ctlverification","author":"kesten","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"3","first-page":"193","article-title":"Symbolic model checking without bdds","author":"biere","year":"1999","journal-title":"TACAS Ser LNCS"},{"key":"2","first-page":"825","volume":"185","author":"barrett","year":"2009","journal-title":"Satisfiability Modulo Theories Ser Frontiers in Artificial Intelligence and Applications"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"1"},{"key":"10","first-page":"291","article-title":"Model checking and transitive-closure logic","volume":"1254","author":"immerman","year":"1997","journal-title":"CAV Ser LNCS"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"6","first-page":"400","article-title":"Symbolic model checking of infinite state systems using presburger arithmetic","volume":"1254","author":"bultan","year":"1997","journal-title":"CAV Ser LNCS"},{"key":"5","first-page":"127","article-title":"Checking safety properties using induction and a sat-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"FM Ser LNCS"},{"key":"4","first-page":"51","article-title":"Bounded model checking of infinite state systems","author":"sch\ufffdle","year":"2007","journal-title":"Formal Methods in System Design"},{"key":"9","article-title":"Reducing ctl-live model checking to semantic entailment in first-order logic (version 1","author":"vakili","year":"2014","journal-title":"Cheriton School of Comp Sci"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2014,10,21]]},"location":"Lausanne, Switzerland","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\/06987616.pdf?arnumber=6987616","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T02:54:05Z","timestamp":1498186445000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987616\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":14,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987616","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}