{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:38:23Z","timestamp":1760783903191,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987611","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"179-186","source":"Crossref","is-referenced-by-count":8,"title":["Turbo-charging Lemmas on demand with don't care reasoning"],"prefix":"10.1109","author":[{"given":"Aina","family":"Niemetz","sequence":"first","affiliation":[]},{"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"Lemmas on demand for lambdas","volume":"13","author":"preiner","year":"2013","journal-title":"DIFTS"},{"key":"17","first-page":"2013","article-title":"Factoring out assumptions to speed up mus extraction","volume":"13","author":"lagniez","year":"0","journal-title":"SAT"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-7548-5"},{"key":"15","article-title":"Exploiting qbf duality on a circuit representation","volume":"10","author":"goultiaeva","year":"2010","journal-title":"AAAI"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.172"},{"key":"13","article-title":"Efficient implementation of property directed reachability","volume":"11","author":"e\ufffdn","year":"2011","journal-title":"FMCAD"},{"key":"14","article-title":"An extensible sat-solver","volume":"4","author":"e\ufffdn","year":"2004","journal-title":"SAT"},{"key":"11","article-title":"Lazy theorem proving for bounded model checking over infinite domains","volume":"2","author":"de moura","year":"2002","journal-title":"CADE"},{"key":"12","article-title":"Computing prime implicants","volume":"13","author":"d\ufffdharbe","year":"2013","journal-title":"FMCAD"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.042"},{"key":"20","article-title":"Lazy satisability modulo theories","volume":"3","author":"sebastiani","year":"2007","journal-title":"JSAT"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_25"},{"journal-title":"Automatic Formal Verification of Control Logic in Hardware Designs","year":"2009","author":"andraus","key":"1"},{"journal-title":"Relevancy Propagation","year":"2007","author":"de moura","key":"10"},{"key":"7","article-title":"Lemmas on demand for the extensional theory of arrays","volume":"6","author":"brummayer","year":"2009","journal-title":"JSAT"},{"key":"6","article-title":"Semi-formal bounded model checking","volume":"2","author":"bingham","year":"2002","journal-title":"CAV"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.32"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679404"},{"key":"9","article-title":"Counterexample guided abstraction refinement","volume":"0","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"8","article-title":"Incremental formal verification of hardware","volume":"11","author":"chockler","year":"2011","journal-title":"FMCAD"}],"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\/06987611.pdf?arnumber=6987611","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:51:23Z","timestamp":1490316683000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987611\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987611","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}