{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T05:43:00Z","timestamp":1749620580362,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/iccad.2004.1382631","type":"proceedings-article","created":{"date-parts":[[2005,2,22]],"date-time":"2005-02-22T15:29:50Z","timestamp":1109086190000},"page":"510-517","source":"Crossref","is-referenced-by-count":50,"title":["Efficient SAT-based unbounded symbolic model checking using circuit cofactoring"],"prefix":"10.1109","author":[{"given":"M.K.","family":"Ganai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Ashar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2002.1012722"},{"key":"17","article-title":"On-the-fly compression of logical circuits","author":"ganai","year":"2000","journal-title":"Proceedings of International Workshop on Logic Synthesis"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"15","article-title":"SATORI An efficient sequential SAT solver for circuits","author":"iyer","year":"2003","journal-title":"International Conference on Computer-Aided Design"},{"key":"16","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"Computer-Aided Verification"},{"key":"13","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","author":"mcmillan","year":"2002","journal-title":"Computer-Aided Verification"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253708"},{"key":"11","first-page":"354","article-title":"SAT-based image computation with application in reachability analysis","author":"gupta","year":"2000","journal-title":"Proceedings of Conference on Formal Methods in Computer-aided Design"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776043"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"20","first-page":"272","article-title":"SATO: An efficient propositional prover","volume":"1249","author":"zhang","year":"1997","journal-title":"Proc Int Conf Automated Deduction"},{"key":"22","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":"23","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/FTCSH.1995.532658"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156197"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2003.1257811"},{"journal-title":"The VIS Home Page","year":"0","key":"27"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2002.995020"},{"key":"2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-40922-X_23","article-title":"SAT-based verification without state space traversal","author":"bjesse","year":"2000","journal-title":"Proceedings of Conference on Formal Methods in Computer-aided Design"},{"key":"10","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/10722167_13","article-title":"Combining decision diagrams and SAT procedures for efficient symbolic model checking","volume":"1855","author":"williams","year":"2000","journal-title":"Proc Int Conf Computer Aided Verification"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"7","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":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"5"},{"key":"4","article-title":"Symbolic reachability analysis based on (SAT)-solvers","author":"abdulla","year":"2000","journal-title":"Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS)"},{"key":"9","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","author":"gupta","year":"2003","journal-title":"Computer-Aided Verification"},{"key":"8","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"}],"event":{"name":"ICCAD 2004. International Conference on Computer Aided Design","acronym":"ICCAD-04","location":"San Jose, CA, USA"},"container-title":["IEEE\/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9494\/30133\/01382631.pdf?arnumber=1382631","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T15:11:24Z","timestamp":1548688284000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1382631\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/iccad.2004.1382631","relation":{},"subject":[]}}