{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:07Z","timestamp":1776316927552,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540001164","type":"print"},{"value":"9783540361268","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_3","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"33-51","source":"Crossref","is-referenced-by-count":62,"title":["Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis"],"prefix":"10.1007","author":[{"given":"Pankaj","family":"Chauhan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Kukula","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Sapra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Felice Balarin and Alberto L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Proceedings of CAV\u201993, pages 29\u201340, 1993.","DOI":"10.1007\/3-540-56922-7_4"},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proceedings of Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u201999)","author":"A. Biere","year":"1999","unstructured":"Armin Biere, Alexandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Proceedings of Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u201999), number 1579 in LNCS, 1999."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, Jim Kukula, Tom Shiple, Helmut Veith, and Dong Wang. Non-linear quantification scheduling in image computation. In Proceedings of ICCAD\u201901, pages 293\u2013298, November 2001.","DOI":"10.1109\/ICCAD.2001.968636"},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/3-540-44798-9_24","volume-title":"Proceedings of CHARME\u201901","author":"P. Chauhan","year":"2001","unstructured":"Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, Jim Kukula, Helmut Veith, and Dong Wang. Using combinatorial optimization methods for quantification scheduling. In Tiziana Margaria and Tom Melham, editors, Proceedings of CHARME\u201901, volume 2144 of LNCS, pages 293\u2013309, September 2001."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Proceedings of the International Conference on Computer-Aided Verification (CAV\u201999)","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings of the International Conference on Computer-Aided Verification (CAV\u201999), number 1633 in Lecture Notes in Computer Science, pages 495\u2013499. Springer, July 1999."},{"key":"3_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Proceedings of CAV","author":"E. M. Clarke","year":"2000","unstructured":"E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, Proceedings of CAV, volume 1855 of LNCS, pages 154\u2013169, July 2000."},{"key":"3_CR7","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Edmund Clarke, Anubhav Gupta, James Kukula, and Ofer Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In Proceedings of CAV\u201902, 2002. To appear.","DOI":"10.1007\/3-540-45657-0_20"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Edmund Clarke, Somesh Jha, Yuan Lu, and Helmut Veith. Tree-like counterexamples in model checking. In Proceedings of the 17 th Annual IEEE Symposium on Logic in Computer Science (LICS\u201902), 2002. To appear.","DOI":"10.1109\/LICS.2002.1029814"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Satyaki Das and David Dill. Successive approximation of abstract transition relations. In Proceedings of the 16 th Annual IEEE Symposium on Logic in Computer Science (LICS\u201901), 2001.","DOI":"10.1109\/LICS.2001.932482"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Shankar G. Govindaraju and David L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In Proceedings of ICCAD\u201900, San Jose, CA, November 2000.","DOI":"10.21236\/ADA401014"},{"key":"3_CR12","unstructured":"P.-H. Ho, T. Shiple, K. Harer, J. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long. Smart simulation using collaborative formal and simulation engines. In Proceedings of ICCAD\u201900, November 2000."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-Aided Verification of Co-ordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"J. Lind-Nielsen and H. Andersen. Stepwise CTL model checking of state\/event systems. In N. Halbwachs and D. Peled, editors, Proceedings of the International Conference on Computer Aided Verification (CAV\u201999), 1999.","DOI":"10.1007\/3-540-48683-6_28"},{"key":"3_CR15","unstructured":"David E. Long. Model checking, abstraction and compositional verification. PhD thesis, Carnegie Mellon University, 1993. CMU-CS-93-178."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference (DAC\u201901), pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Abelardo Pardo and Gary D. Hachtel. Incremental CTL model checking using BDD subsetting. In Proceedings of the Design Automation Conference (DAC\u201998), pages 457\u2013462, June 1998.","DOI":"10.1145\/277044.277171"},{"key":"3_CR18","unstructured":"J. P. Marques Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. Technical Report CSE-TR-292-96, Computer Science and Engineering Division, Department of EECS, Univ. of Michigan, April 1996."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Dong Wang, Pei-Hsin Ho, Jiang Long, James Kukula, Yunshan Zhu, Tony Ma, and Robert Damiano. Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In Proceedings of the DAC, pages 35\u201340, 2001.","DOI":"10.1145\/378239.378260"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Hantao Zhang. SATO: An efficient propositional prover. In Proceedings of the Conference on Automated Deduction (CADE\u201997), pages 272\u2013275, 1997.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"3_CR21","unstructured":"Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in a Boolean satisfiability solver. In Proceedings ofICCAD\u201901, November 2001."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:24:53Z","timestamp":1739993093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}