{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T03:17:22Z","timestamp":1725419842435},"reference-count":36,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,11]]},"DOI":"10.1109\/iccad.2010.5653863","type":"proceedings-article","created":{"date-parts":[[2010,12,10]],"date-time":"2010-12-10T22:29:13Z","timestamp":1292020153000},"page":"786-793","source":"Crossref","is-referenced-by-count":3,"title":["Efficient state space exploration: Interleaving stateless and state-based model checking"],"prefix":"10.1109","author":[{"given":"Malay K.","family":"Ganai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weihong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","article-title":"Algorithms for approximate fsm traversal based on state space decomposition","author":"cho","year":"1996","journal-title":"IEEE Trans on CAD"},{"key":"35","doi-asserted-by":"crossref","DOI":"10.1021\/je060013d","article-title":"Disjunctive image computation for embedded software verification","author":"wang","year":"2006","journal-title":"DATE"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_20"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233662"},{"journal-title":"CUDD CU Decision Digram Package University of Colorado at Boulder","year":"0","author":"somenzi","key":"18"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403578"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_6"},{"key":"16","article-title":"A fast linear-arithmetic solver for DPLL(T)","author":"dutertre","year":"2006","journal-title":"CAV"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_40"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233664"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/332740.332746"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2006.1695896"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2009.5185373"},{"key":"20","article-title":"A library for composite symbolic representations","author":"yavuz-kahveci","year":"2001","journal-title":"TACAS"},{"journal-title":"SRI Yices An SMT Solver","year":"0","key":"22"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.41"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277201"},{"key":"26","article-title":"On combining formal and informal verification","author":"yuan","year":"1997","journal-title":"CAV"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2006.244050"},{"key":"28","article-title":"Abstraction and bdds complement SAT-based bmc in diver","author":"gupta","year":"2003","journal-title":"CAV"},{"key":"29","article-title":"And sat-based model checking","author":"mcmillan","year":"2003","journal-title":"CAV"},{"key":"3","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"1"},{"key":"30","article-title":"Exploiting target enlargement and dynamic abstraction within mixed bdd and sat invariant checking","author":"bischoff","year":"2004","journal-title":"BMC Workshop"},{"key":"7","article-title":"The SLAM toolkit","author":"ball","year":"2001","journal-title":"CAV"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391507"},{"key":"5","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-69167-1","author":"ganai","year":"2007","journal-title":"SAT-based Scalable Formal Verification Solutions"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403577"},{"key":"4","article-title":"Checking safety properties using induction and a SAT solver","author":"sheeran","year":"2000","journal-title":"FMCAD"},{"key":"9","article-title":"F-Soft: Software verification platform. In","author":"ivanc?ic?","year":"2005","journal-title":"CAV"},{"key":"8","article-title":"A tool, for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"TACAS"}],"event":{"name":"2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)","start":{"date-parts":[[2010,11,7]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2010,11,11]]}},"container-title":["2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5638200\/5648785\/05653863.pdf?arnumber=5653863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T13:08:12Z","timestamp":1497877692000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5653863\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11]]},"references-count":36,"URL":"https:\/\/doi.org\/10.1109\/iccad.2010.5653863","relation":{},"subject":[],"published":{"date-parts":[[2010,11]]}}}