{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:01:09Z","timestamp":1777125669746,"version":"3.51.4"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/iccad.2003.1257811","type":"proceedings-article","created":{"date-parts":[[2004,5,13]],"date-time":"2004-05-13T10:43:37Z","timestamp":1084445017000},"page":"416-423","source":"Crossref","is-referenced-by-count":34,"title":["Iterative abstraction using SAT-based BMC with proof analysis"],"prefix":"10.1109","author":[{"given":"A.","family":"Gupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Ganai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Zijiang Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Ashar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"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 the Conference on Design Automation and Test in Europe (DATE)"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253718"},{"key":"ref12","article-title":"Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis","author":"chauhan","year":"2002","journal-title":"Proceedings of Conference on Formal Methods in CAD (FMCAD)"},{"key":"ref13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X_2","article-title":"Automatic Abstraction Without Counterexamples","author":"mcmillan","year":"2003","journal-title":"Proc Tools Algorithms Constr Anal Syst"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_20"},{"key":"ref17","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"ref18","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":"Proc Conf Computer-Aided Verification"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156104"},{"key":"ref4","article-title":"Symbolic Model Checking without BDDs","volume":"1579","author":"biere","year":"1999","journal-title":"Proceedings of Workshop on Tools and Algorithms for Analysis and Construction of Systems (TACAS)"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: A Search Algorithm for Propositional Satisfiability","volume":"48","author":"marques-silva","year":"1999","journal-title":"IEEE Transactions on Computers"},{"key":"ref5","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-40922-X_8","article-title":"Checking Safety Properties using Induction and a SAT Solver","author":"sheeran","year":"2000","journal-title":"Proceedings of Conference on Formal Methods in Computer-aided Design"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2002.998262"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref9","article-title":"Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver","author":"ganai","year":"2002","journal-title":"Proceedings of the Design Automation Conference"},{"key":"ref1","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref20","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45657-0_20","article-title":"SAT based abstraction-refinement using ILP and machine learning techniques","author":"clarke","year":"2002","journal-title":"Proc Conf Computer-Aided Verification"},{"key":"ref22","doi-asserted-by":"crossref","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":"Proceedings of Conference on Computer-Aided Verification"},{"key":"ref21","article-title":"Lazy Abstraction","author":"majumdar","year":"2002","journal-title":"Proc Conf Principles of Programming Languages"},{"key":"ref24","article-title":"Efficient Conflict Driven Learning in a Boolean Satisfiability Solver","author":"zhang","year":"2001","journal-title":"Proceedings of the International Conference on Computer-Aided Design"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2001.968635"}],"event":{"name":"ICCAD-2003. International Conference on Computer Aided Design","location":"San Jose, CA, USA","acronym":"ICCAD-03"},"container-title":["ICCAD-2003. International Conference on Computer Aided Design (IEEE Cat. No.03CH37486)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8895\/28127\/01257811.pdf?arnumber=1257811","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,17]],"date-time":"2018-05-17T12:09:09Z","timestamp":1526558949000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1257811\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/iccad.2003.1257811","relation":{},"subject":[]}}