{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T23:32:47Z","timestamp":1729639967559,"version":"3.28.0"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987594","type":"proceedings-article","created":{"date-parts":[[2014,12,30]],"date-time":"2014-12-30T20:00:39Z","timestamp":1419969639000},"page":"43-50","source":"Crossref","is-referenced-by-count":8,"title":["Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checking"],"prefix":"10.1109","author":[{"given":"G.","family":"Cabodi","sequence":"first","affiliation":[]},{"given":"M.","family":"Palena","sequence":"additional","affiliation":[]},{"given":"P.","family":"Pasini","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"22","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-52148-8_30","article-title":"Verification of sequential machines based on symbolic execution","volume":"407","author":"coudert","year":"1989","journal-title":"Lecture Notes in Computer Science"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763056"},{"key":"23","first-page":"173","article-title":"Lazy abstraction and sat-based reachability in hardware model checking","author":"vizel","year":"2012","journal-title":"Proc Formal Methods in Computer-Aided Design"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0123-3"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_38"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"13","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_15"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.289"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"journal-title":"The Minisat SAT Solver","year":"2009","author":"e\ufffdn","key":"20"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1959.9.129"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681563"},{"key":"7","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/11560548_33","article-title":"Improvements to the implementation of interpolant-based model checking","volume":"3725","author":"marques-silva","year":"2005","journal-title":"Proc Correct Hardware Design and Ver-ification Methods Ser LNCS"},{"key":"6","first-page":"39","article-title":"Interpolation and sat-based model checking","volume":"3725","author":"mcmillan","year":"2005","journal-title":"Proc Computer Aided Verification Ser LNCS"},{"journal-title":"The Model Checking Competition Web Page","year":"0","author":"biere","key":"5"},{"key":"4","first-page":"70","article-title":"Sat-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"VMCAI"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1297666.1297669"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_10"}],"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\/06987594.pdf?arnumber=6987594","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T22:54:05Z","timestamp":1498172045000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987594\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987594","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}