{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T17:18:35Z","timestamp":1730222315162,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1109\/fmcad.2016.7886657","type":"proceedings-article","created":{"date-parts":[[2017,3,27]],"date-time":"2017-03-27T22:52:44Z","timestamp":1490655164000},"page":"25-32","source":"Crossref","is-referenced-by-count":2,"title":["Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening"],"prefix":"10.1109","author":[{"given":"G.","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. E.","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Palena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Pasini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Vendraminetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref30","first-page":"24","article-title":"Abc: An academic industrial-strength verification tool","author":"brayton","year":"2010","journal-title":"CAV"},{"key":"ref10","article-title":"Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications","author":"zhang","year":"2003","journal-title":"Proc of DATE"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0229-0"},{"key":"ref12","first-page":"1","article-title":"A proof-sensitive approach for small propositional interpolants","author":"alt","year":"2015","journal-title":"Verified Software Theories Tools and Experiments-Revised Selected Papers"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"ref14","first-page":"532","article-title":"DAG-Aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis","author":"brayton","year":"2006","journal-title":"Proc of DAC"},{"key":"ref15","first-page":"67","article-title":"Dominator-based partitioning for delay optimization","author":"neres","year":"2006","journal-title":"Proceedings of the 16th ACM Great Lakes symposium on VLSI  - GLSVLSI '06"},{"key":"ref16","article-title":"Cut Sweeping","author":"e\u00e9n","year":"2007","journal-title":"Cadence Research Labs Berkeley USA Tech Rep"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1997.597155"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"ref28","first-page":"39","article-title":"Interpolation and SAT-Based Model Checking","volume":"3725","author":"mcmillan","year":"2005","journal-title":"Proc of CAV Ser LNCS"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964021"},{"key":"ref27","first-page":"181","article-title":"A single-instance incremental sat formulation of proof- and counterexample-based abstraction","author":"een","year":"2010","journal-title":"Proc of FMCAD"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_10"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0123-3"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_33"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2008.4681563"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1297666.1297669"},{"key":"ref2","first-page":"1","article-title":"Interpolation and SAT-Based Model Checking","volume":"2725","author":"mcmillan","year":"2003","journal-title":"Proc of CAV Ser LNCS"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_15"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"article-title":"The Model Checking Competition","year":"0","author":"biere","key":"ref20"},{"key":"ref22","article-title":"Sat-based complete don't-care computation for network optimization","volume":"abs 710 4695","author":"mishchenko","year":"2007","journal-title":"CoRR"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1991.185319"},{"key":"ref24","article-title":"Computer Aided Verification of Coordinating Processes","author":"kurshan","year":"1994","journal-title":"Princeton University Press"},{"key":"ref23","first-page":"250","article-title":"Applying sat methods in unbounded symbolic model checking","volume":"2404","author":"mcmillan","year":"2002","journal-title":"Proc of CAV"},{"key":"ref26","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"Proc of CAV"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.286"}],"event":{"name":"2016 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2016,10,3]]},"location":"Mountain View, CA, USA","end":{"date-parts":[[2016,10,6]]}},"container-title":["2016 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7879555\/7886641\/07886657.pdf?arnumber=7886657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,13]],"date-time":"2017-12-13T14:49:42Z","timestamp":1513176582000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7886657\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2016.7886657","relation":{},"subject":[],"published":{"date-parts":[[2016,10]]}}}