{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T21:45:40Z","timestamp":1768340740159,"version":"3.49.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/iccad.2004.1382630","type":"proceedings-article","created":{"date-parts":[[2005,2,22]],"date-time":"2005-02-22T20:29:50Z","timestamp":1109104190000},"page":"502-509","source":"Crossref","is-referenced-by-count":13,"title":["Incremental deductive & inductive reasoning for SAT-based bounded model checking"],"prefix":"10.1109","author":[{"family":"Liang Zhang","sequence":"first","affiliation":[]},{"given":"M.R.","family":"Prasad","sequence":"additional","affiliation":[]},{"given":"M.S.","family":"Hsiao","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"key":"ref11","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-540-45069-6_20","article-title":"Abstraction and BDDs Complement SAT-based BMC in DiVer","volume":"2725","author":"gupta","year":"2003","journal-title":"Proc Conf Computer-Aided Verification"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"824","DOI":"10.1145\/775832.776040","article-title":"Learning from BDDs in SAT-based Bounded Model Checking","author":"gupta","year":"2003","journal-title":"Proc 40th Design Automation Conf"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref18","article-title":"SIS: A System for Sequential Circuit Synthesis","author":"sentovich","year":"1998","journal-title":"Technical Report UCB\/ERL M92\/41"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2003.1250266"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref27","doi-asserted-by":"crossref","DOI":"10.1109\/DATE.2003.1253717","article-title":"Validating SAT Solvers using an Independent Resolution-based Checker: Practical Implementations and Other Applications","author":"zhang","year":"2003","journal-title":"Proc of the Design Automation and Test in Europe (DATE)"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253720"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","article-title":"Benefits of Bounded Model Checking in an Industrial Setting","volume":"2102","author":"copti","year":"2001","journal-title":"Proc of the 13 th Intl Conf on Computer Aided Verification"},{"key":"ref5","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2002.1167572"},{"key":"ref7","article-title":"Temporal Induction by Incremental SAT Solving","author":"e\u00e9n","year":"2003","journal-title":"Proc Int'l Workshop Bounded Model Checking"},{"key":"ref2","first-page":"372","article-title":"SAT-based Verification without State Space Traversal","volume":"1954","author":"bjesse","year":"2000","journal-title":"Proc of the 3rd lntl Conf on Formal Methods in CAD"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2002.995020"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_4"},{"key":"ref20","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","volume":"1954","author":"sheeran","year":"2000","journal-title":"Proc Int Conf Formal Methods CAD"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","article-title":"The VIS Group, VIS:A system for Verification and Synthesis","volume":"1102","author":"alur","year":"1996","journal-title":"Proc of the 8th Intl Conf on Com puter Aided Verification"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","article-title":"Accelerating Bounded Model Checking of Safety Formulas","volume":"24","author":"shtrichman","year":"2004","journal-title":"Formal Methods in System Design"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996713"},{"key":"ref26","first-page":"272","article-title":"SATO: An Efficient Propositional Prover","author":"zhang","year":"1997","journal-title":"Proc Ninth Intl Conf on Automated Deduction"},{"key":"ref25","year":"2003"}],"event":{"name":"ICCAD 2004. International Conference on Computer Aided Design","location":"San Jose, CA, USA","acronym":"ICCAD-04"},"container-title":["IEEE\/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9494\/30133\/01382630.pdf?arnumber=1382630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T09:50:02Z","timestamp":1625478602000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1382630\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/iccad.2004.1382630","relation":{},"subject":[]}}