{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T15:38:43Z","timestamp":1787499523436,"version":"build-2736575974"},"reference-count":88,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. IEEE"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1109\/jproc.2015.2455034","type":"journal-article","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T14:40:30Z","timestamp":1440600030000},"page":"2021-2035","source":"Crossref","is-referenced-by-count":94,"title":["Boolean Satisfiability Solvers and Their Applications in Model Checking"],"prefix":"10.1109","volume":"103","author":[{"given":"Yakir","family":"Vizel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0183-4"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9156-3"},{"key":"ref76","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-642-31424-7_18","article-title":"Leveraging interpolant strength in model checking","volume":"7358","author":"rollini","year":"2012","journal-title":"Computer Aided Verification"},{"key":"ref77","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"Formal Methods in Computer-Aided Design"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"ref39","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"een","year":"0","journal-title":"Proc FMCAD"},{"key":"ref75","first-page":"337","article-title":"Specification and verification of concurrent systems in CESAR","author":"queille","year":"0","journal-title":"Proc Int Symp Programming"},{"key":"ref38","first-page":"102","article-title":"Effective preprocessing in SAT through variable and clause elimination","volume":"3569","author":"e\u00e9n","year":"2005","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_33"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref60","article-title":"Boolean satisfiability solvers: Techniques and extensions","author":"malik","year":"2012","journal-title":"Software Safety and Security—Tools for Analysis and Verification"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref61","first-page":"530","article-title":"Chaff: Engineering an efficient SAT solver","author":"malik","year":"0","journal-title":"Proc DAC"},{"key":"ref63","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","article-title":"Applying SAT methods in unbounded symbolic model checking","volume":"2404","author":"mcmillan","year":"2002","journal-title":"Computer Aided Verification"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","article-title":"Counterexample-guided abstraction refinement","volume":"1855","author":"clarke","year":"2000","journal-title":"Computer Aided Verification"},{"key":"ref64","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","article-title":"Interpolation and SAT-based model checking","volume":"2725","author":"mcmillan","year":"2003","journal-title":"Computer Aided Verification"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref65","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/11817963_14","article-title":"Lazy abstraction with interpolants","volume":"4144","author":"mcmillan","year":"2006","journal-title":"Computer Aided Verification"},{"key":"ref66","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","article-title":"Automatic abstraction without counterexamples","volume":"2619","author":"mcmillan","year":"2003","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref67","author":"mcmillan","year":"1992","journal-title":"The SMV System"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.286"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_3"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/11560548_20","article-title":"An analysis of SAT-based model checking techniques in an industrial environment","volume":"3725","author":"amla","year":"2005","journal-title":"Correct Hardware Design and Verification Methods"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987594"},{"key":"ref22","first-page":"135","article-title":"Incremental formal verification of hardware","author":"chockler","year":"0","journal-title":"Proc FMCAD"},{"key":"ref21","first-page":"334","article-title":"The nuXmv symbolic model checker","volume":"8559","author":"cavada","year":"2014","journal-title":"Computer Aided Verification"},{"key":"ref24","article-title":"New techniques that improve MACE-style finite model finding","author":"claessen","year":"0","journal-title":"Proc Model Comput —Principles Algor Appl"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838559"},{"key":"ref26","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"ref50","first-page":"2318","article-title":"The effect of restarts on the efficiency of clause learning","author":"huang","year":"0","journal-title":"Proc IJCAI"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/ISTCS.1993.253477"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_56"},{"key":"ref57","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"ref55","first-page":"674","article-title":"Dynamic restart policies","author":"kautz","year":"0","journal-title":"Proc AAAI\/IAAI"},{"key":"ref54","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/11513988_6","article-title":"Interpolant-based transition relation approximation","volume":"3576","author":"jhala","year":"2005","journal-title":"Computer Aided Verification"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","article-title":"PicoSAT essentials","volume":"4","author":"biere","year":"2008","journal-title":"J Satisfiability Boolean Modeling Comput"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_1"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"ref12","first-page":"193","article-title":"Symbolic model checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref13","volume":"185","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"SAT-based model checking without unrolling","volume":"6538","author":"bradley","year":"2011","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"ABC: An academic industrial-strength verification tool","volume":"6174","author":"brayton","year":"2010","journal-title":"Computer Aided Verification"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113767"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_24"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0123-3"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_23"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763056"},{"key":"ref80","article-title":"On the complexity of proofs in propositional logics","volume":"2","author":"tseitin","year":"1983","journal-title":"Automation of Reasoning Classical Papers on Computational Logic"},{"key":"ref4","first-page":"118","article-title":"Refining restarts strategies for SAT and UNSAT","volume":"7514","author":"audemard","year":"2012","journal-title":"Constraint Programming"},{"key":"ref3","first-page":"399","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"0","journal-title":"Proc IJCAI"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","article-title":"Towards understanding and harnessing the potential of clause learning","volume":"22","author":"beame","year":"2004","journal-title":"J Artif Intell Res"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679404"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.168"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022905120346"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_5"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030832"},{"key":"ref87","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","article-title":"SATzilla: Portfolio-based algorithm selection for SAT","volume":"32","author":"xu","year":"2008","journal-title":"J Artif Intell Res"},{"key":"ref88","first-page":"10880","article-title":"Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications","author":"zhang","year":"0","journal-title":"Proc IEEE DATE"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79719-7_4"},{"key":"ref46","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v34i2.2450","article-title":"Seven challenges in parallel SAT solving","volume":"34","author":"hamadi","year":"2013","journal-title":"AI Mag"},{"key":"ref45","article-title":"DRUPing for interpolants","author":"gurfinkel","year":"0","journal-title":"Proc FMCAD"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"ref42","article-title":"Generalizations of watched literals for backtracking search","author":"gelder","year":"0","journal-title":"Proc ISAIM"},{"key":"ref41","first-page":"333","article-title":"An extensible SAT-solver","volume":"2919","author":"e\u00e9n","year":"2004","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253718"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/3-540-45139-0_2","article-title":"Model checking if your life depends on it: A view from intel's trenches","volume":"2057","author":"gerth","year":"2001","journal-title":"Model Checking and Software Verification"}],"container-title":["Proceedings of the IEEE"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/5\/7302610\/07225110.pdf?arnumber=7225110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,10]],"date-time":"2021-10-10T22:35:53Z","timestamp":1633905353000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7225110\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":88,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/jproc.2015.2455034","relation":{},"ISSN":["0018-9219","1558-2256"],"issn-type":[{"value":"0018-9219","type":"print"},{"value":"1558-2256","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}