{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:10:46Z","timestamp":1774987846804,"version":"3.50.1"},"reference-count":49,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1109\/tcad.2006.873897","type":"journal-article","created":{"date-parts":[[2006,10,30]],"date-time":"2006-10-30T17:35:30Z","timestamp":1162229730000},"page":"2297-2316","source":"Crossref","is-referenced-by-count":13,"title":["Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement"],"prefix":"10.1109","volume":"25","author":[{"given":"C.","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.D.","family":"Hachtel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-540-30494-4_19","article-title":"A hybrid of counterexample-based and proof-based abstraction","author":"amla","year":"2004","journal-title":"Proc Formal Methods in Computer-Aided Design"},{"key":"ref38","first-page":"254","article-title":"An analysis of sat-based model checking techniques in an industrial environment","author":"amla","year":"2005","journal-title":"Proc CHARME"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996630"},{"key":"ref31","first-page":"176","article-title":"Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation","volume":"2619","author":"glusman","year":"2003","journal-title":"Proc TACAS"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/343647.343831"},{"key":"ref37","first-page":"183","article-title":"Lazy constraints and SAT heuristics for proof-based abstraction","author":"gupta","year":"2005","journal-title":"Proc Int Conf VLSI Des"},{"key":"ref36","year":"0"},{"key":"ref35","first-page":"428","article-title":"VIS: A system for verification and synthesis","volume":"1102","author":"brayton","year":"1996","journal-title":"Proc CAV"},{"key":"ref34","first-page":"880","article-title":"Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications","author":"zhang","year":"2003","journal-title":"Proc DATE"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_28"},{"key":"ref27","first-page":"76","article-title":"Tearing based abstraction for CTL model checking","author":"lee","year":"1996","journal-title":"Proc Int Conf Comput -Aided Des"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277171"},{"key":"ref2","first-page":"112","article-title":"Fine-grain abstraction and sequential don't cares for large scale model checking","author":"wang","year":"2004","journal-title":"Proc Int Conf Comput Des"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.873897"},{"key":"ref20","first-page":"338","article-title":"Bisimulation and model checking","volume":"1703","author":"fisler","year":"1999","journal-title":"Proc CHARME"},{"key":"ref22","author":"long","year":"1993","journal-title":"Model checking abstraction and compositional verification"},{"key":"ref21","first-page":"29","article-title":"An iterative approach to language containment","volume":"697","author":"balarin","year":"1993","journal-title":"Proc CAV"},{"key":"ref24","author":"kurshan","year":"1994","journal-title":"Computer-aided Verification of Coordinating Processes"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1109\/43.552080","article-title":"Algorithms for approximate FSM traversal based on state space decomposition","volume":"15","author":"cho","year":"1996","journal-title":"IEEE Trans Comput -Aided Des Integr Circuits Syst"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref25","first-page":"423","article-title":"COSPAN","volume":"1102","author":"hardin","year":"1996","journal-title":"Proc CAV"},{"key":"ref10","first-page":"2","article-title":"Automatic abstraction without counterexamples","volume":"2619","author":"mcmillan","year":"2003","journal-title":"Proc TACAS"},{"key":"ref11","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 Design Automation Conf"},{"key":"ref40","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82546-0"},{"key":"ref13","first-page":"518","article-title":"Efficient computation of small abstraction refinements","author":"li","year":"2004","journal-title":"Proc Int Conf Comput -Aided Des"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0169-2"},{"key":"ref15","first-page":"502","article-title":"Incremental deductive and inductive reasoning for SAT-based bounded model checking","author":"zhang","year":"2004","journal-title":"Proc Int Conf Comput -Aided Des"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065776"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref18","first-page":"481","article-title":"An algebraic definition of simulation between programs","author":"milner","year":"1971","journal-title":"Proc 2nd Int Joint Conf Artif Intell"},{"key":"ref19","first-page":"255","article-title":"Checking for language inclusion using simulation relations","volume":"575","author":"dill","year":"1991","journal-title":"Proc CAV"},{"key":"ref4","author":"mcmillan","year":"1994","journal-title":"Symbolic Model Checking"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156104"},{"key":"ref5","first-page":"154","article-title":"Counterexample-guided abstraction refinement","volume":"1855","author":"clarke","year":"2000","journal-title":"Proc CAV"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-36126-X_3","volume":"2517","author":"chauhan","year":"2002","journal-title":"Formal Methods in Computer Aided Design"},{"key":"ref7","first-page":"265","article-title":"SAT based abstraction-refinement using ILP and machine learning","volume":"2404","author":"clarke","year":"2002","journal-title":"Proc CAV"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"ref9","first-page":"65","article-title":"Symbolic localization reduction with reconstruction layering and backtracking","volume":"2404","author":"barner","year":"2002","journal-title":"Proc CAV"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337305"},{"key":"ref45","first-page":"445","article-title":"Fate and free will in error traces","volume":"2280","author":"jin","year":"2002","journal-title":"Proc TACAS"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/EDAC.1990.136620"},{"key":"ref47","first-page":"41","article-title":"Least fixpoint approximations for reachability analysis","author":"moon","year":"1999","journal-title":"Proc Int Conf Comput -Aided Des"},{"key":"ref42","first-page":"206","article-title":"Abstraction and BDDs complement SAT-based BMC in DiVer","volume":"2725","author":"gupta","year":"2003","journal-title":"Proc CAV"},{"key":"ref41","article-title":"Efficient BDD algorithms for FSM synthesis and verification","author":"ranjan","year":"1995","journal-title":"Int Workshop Logic Synthesis"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253720"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/43\/36103\/01715417.pdf?arnumber=1715417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:06Z","timestamp":1638218406000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/1715417\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":49,"journal-issue":{"issue":"11"},"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/tcad.2006.873897","relation":{},"ISSN":["0278-0070"],"issn-type":[{"value":"0278-0070","type":"print"}],"subject":[],"published":{"date-parts":[[2006,11]]}}}