{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:33:01Z","timestamp":1725733981767},"reference-count":14,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.23919\/fmcad.2017.8102252","type":"proceedings-article","created":{"date-parts":[[2017,11,9]],"date-time":"2017-11-09T21:49:00Z","timestamp":1510264140000},"page":"140-147","source":"Crossref","is-referenced-by-count":4,"title":["Learning support sets in IC3 and Quip: The good, the bad, and the ugly"],"prefix":"10.23919","author":[{"given":"Ryan","family":"Berryhill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Ivrii","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Veira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Veneris","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"502","article-title":"An extensible SAT-solver","author":"e\u00e9n","year":"2003","journal-title":"SAT 2003"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_21"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.9"},{"key":"ref3","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"e\u00e9n","year":"2011","journal-title":"ser FMCAD 2011"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/IVSW.2017.8031554"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_38"},{"journal-title":"IImc an Incremental Inductive model checker","year":"0","author":"bradley","key":"ref7"},{"key":"ref2","article-title":"SAT-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"VMCAI"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744921"},{"key":"ref9","first-page":"399","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"2009","journal-title":"Proceedings of the 21st International Joint Conference on Artifical Intelligence (IJCAI)"}],"event":{"name":"2017 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2017,10,2]]},"location":"Vienna","end":{"date-parts":[[2017,10,6]]}},"container-title":["2017 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8093672\/8102222\/08102252.pdf?arnumber=8102252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T22:41:18Z","timestamp":1513032078000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8102252\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":14,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2017.8102252","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}