{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:07:52Z","timestamp":1742396872579},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_13","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"176-191","source":"Crossref","is-referenced-by-count":33,"title":["Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Glusman","sequence":"first","affiliation":[]},{"given":"Gila","family":"Kamhi","sequence":"additional","affiliation":[]},{"given":"Sela","family":"Mador-Haim","sequence":"additional","affiliation":[]},{"given":"Ranan","family":"Fraer","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902)","author":"R. Armoni","year":"2002","unstructured":"R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, and Y. Zbar. The ForSpec temporal logic: A new temporal property-specification language. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902), LNCS. Springer-Verlag, 2002."},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"CAV\u201993","author":"F. Balarin","year":"1993","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In CAV\u201993, LNCS, pages 29\u201340. Springer-Verlag, 1993."},{"key":"13_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/3-540-45657-0_6","volume-title":"CAV\u201902","author":"S. Barner","year":"2002","unstructured":"S. Barner, D. Geist, and A. Gringauze. Symbolic localization reduction with reconstruction layering and backtracking. In E. Brinksma and K. G. Larsen, editors, CAV\u201902, volume 2404 of LNCS, pages 65\u201377. Springer-Verlag, 2002."},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201999)","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201999), volume 1579 of LNCS, pages 193\u2013207. Springer-Verlag, 1999."},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","first-page":"454","volume-title":"CAV\u201901","author":"P. Biesse","year":"2001","unstructured":"P. Biesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessors using satisfiability solvers. In CAV\u201901, volume 2102 of LNCS, pages 454\u2013464. Springer-Verlag, 2001."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"B. Bollobas. Graph Theory. Springer-Verlag, 1979.","DOI":"10.1007\/978-1-4612-9967-7"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"13_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"CAV\u201902","author":"E. M. Clarke","year":"2002","unstructured":"E. M. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In E. Brinksma and K. G. Larsen, editors, CAV\u201902, volume 2404 of LNCS, pages 265\u2013279. Springer-Verlag, 2002."},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACMTransactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACMTransactions on Programming Languages and Systems"},{"key":"13_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"CAV\u201900","author":"E.M. Clarke","year":"2000","unstructured":"E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV\u201900, volume 1855 of LNCS, pages 154\u2013169. Springer-Verlag, 2000."},{"issue":"5","key":"13_CR11","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR12","unstructured":"E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"13_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"CAV\u201901","author":"F. Copty","year":"2001","unstructured":"F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV\u201901, volume 2102 of LNCS, pages 436\u2013453. Springer-Verlag, 2001."},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44798-9_23","volume-title":"Correct Hardware Design and Verification Methods (CHARME\u201901)","author":"F. Copty","year":"2001","unstructured":"F. Copty, A. Irron, O. Weissberg, N.P. Kropp, and G. Kamhi. Efficient debugging in a formal verification environment. In T. Margaria et. al., editor, Correct Hardware Design and Verification Methods (CHARME\u201901), volume 2144 of LNCS, pages 275\u2013292. Springer-Verlag, 2001."},{"key":"13_CR15","doi-asserted-by":"crossref","first-page":"399","DOI":"10.4153\/CJM-1956-045-5","volume":"8","author":"L.R. Ford","year":"1956","unstructured":"L.R. Ford and D.R. Fulkerson. Maximal flow through a network. Canadian Journal of Mathematics, 8:399\u2013404, 1956.","journal-title":"Canadian Journal of Mathematics"},{"key":"13_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/10722167_30","volume-title":"CAV\u201900","author":"R. Fraer","year":"2000","unstructured":"R. Fraer, G. Kamhi, B. Ziv, M. Vardi, and L. Fix. Prioritized traversal: efficient reachability analysis for verication and falsification. In CAV\u201900, volume 1855 of LNCS, pages 389\u2013402. Springer-Verlag, 2000."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"G.S. Govindaraju and D.L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In ICCAD\u201900, 2000.","DOI":"10.1109\/ICCAD.2000.896460"},{"key":"13_CR18","unstructured":"G. Hachtel and F. Somenzi. Synthesis and Verification Algorithms. Kluwer, 1996."},{"key":"13_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"CAV\u201996","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har\u2019el, and R.P. Kurshan. COSPAN. In CAV\u201996, volume 1102 of LNCS, pages 423\u2013427. Springer-Verlag, 1996."},{"key":"13_CR20","unstructured":"R.H. Hardin, R.P. Kurshan, K.L. McMillan, J.A. Reeds, and N.J.A. Sloane. Efficient regression verification. IEE Proc. WODES\u201996, pages 147\u2013150, 1996."},{"key":"13_CR21","unstructured":"P.H. Ho, T. Shiple, K. Harer, J.H. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long. Smart simulation using collaborative formal simulation engines. In ICCAD\u201900, pages 120\u2013126, 2000."},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"J. Jang, I. Moon, and G. Hachtel. Iterative abstraction-based CTL model checking, 2000.","DOI":"10.1145\/343647.343831"},{"issue":"5","key":"13_CR23","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1109\/TC.1984.1676460","volume":"33","author":"B. Krishnamurthy","year":"1984","unstructured":"B. Krishnamurthy. An improved Min-Cut algorithm for partitioning VLSI networks. IEEE Transactions on Computers, 33(5):438\u2013446, 1984.","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR24","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"O. Kupferman and M.Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19:291\u2013314, 2001.","journal-title":"Formal Methods in System Design"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer AidedVerification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"13_CR26","unstructured":"W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing based abstraction for CTL model checking. In ICCAD\u201996, pages 76\u201381, 1996."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"13_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-48683-6_28","volume-title":"CAV\u201999","author":"J. Lind-Nielsen","year":"1999","unstructured":"J. Lind-Nielsen and H.R. Andersen. Stepwise CTL model checking of state\/event systems. In CAV\u201999, volume 1633 of LNCS, pages 316\u2013327. Springer-Verlag, 1999."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, January 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"13_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"CAV\u201900","author":"K.S. Namjoshi","year":"2000","unstructured":"K.S. Namjoshi and R.P. Kurshan. Syntactic program transformations for automatic abstraction. n CAV\u201900, volume 1855 of LNCS, pages 435\u2013449. Springer-Verlag, 2000."},{"key":"13_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-63166-6_5","volume-title":"CAV\u201997","author":"A. Pardo","year":"1997","unstructured":"A. Pardo and G. Hachtel. Automatic abstraction techniques for propositional \u03bc-calculus model checking. In CAV\u201997, volume 1254 of LNCS, pages 12\u201323. Springer-Verlag, 1997."},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"A. Pardo and G. Hachtel. Incremental CTL model checking using BDD subsetting. In Design Automation Conference, pages 457\u2013462, 1998.","DOI":"10.1145\/277044.277171"},{"key":"13_CR33","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Specification and verification of concurrent systems in Cesar","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137 of LNCS, pages 337\u2013351. Springer-Verlag, 1981."},{"key":"13_CR34","unstructured":"R. Rudell. DynamicVariable Ordering for Ordered Binary Decision Diagrams. In ICCAD\u201993, pages 42\u201347. IEEE Computer Society Press, 1993."},{"key":"13_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"TACAS\u201999","author":"V. Rusu","year":"1999","unstructured":"V. Rusu and E. Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In W.R. Cleaveland, editor, TACAS\u201999, volume 1579 of LNCS, pages 178\u2013192. Springer-Verlag, 1999."},{"key":"13_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of LNCS, pages 238\u2013266. Springer-Verlag, 1996."},{"key":"13_CR37","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In 1st Symp. on Logic in Computer Science, pages 332\u2013344, Cambridge, June 1986."},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"D. Wang, P.H. Ho, J. Long, J.H. Kukula, Y. Zhu, T. Ma, and R. Damiano. Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In Design Automation Conference, pages 35\u201340, 2001.","DOI":"10.1145\/378239.378260"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:49:10Z","timestamp":1558982950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}