{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:09Z","timestamp":1776316929236,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008989","type":"print"},{"value":"9783540365778","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_2","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"2-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":93,"title":["Automatic Abstraction without Counterexamples"],"prefix":"10.1007","author":[{"given":"Kenneth L.","family":"McMillan","sequence":"first","affiliation":[]},{"given":"Nina","family":"Amla","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"F. Balarin and A. Sangiovanni-Vincentelli. An iterative approach to language containment. In Computer Aided Verification (CAV\u201993), pages 29\u201340, 1993.","DOI":"10.1007\/3-540-56922-7_4"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"J. Baumgratner, A. Kuehlmann, and J. Abraham. Property checking via structural analysis. In Computer-Aided Verification (CAV 2002), pages 151\u2013165, 2002.","DOI":"10.1007\/3-540-45657-0_12"},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"TACAS\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS\u201999, volume 1579 of LNCS, pages 193\u2013207, 1999."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessor using satisfiability solvers. In Computer Aided Verification (CAV 2001), 2001.","DOI":"10.1007\/3-540-44585-4_44"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154\u2013169, 2000.","DOI":"10.1007\/10722167_15"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In Computer-Aided Verification (CAV 2002), pages 265\u2013279, 2002.","DOI":"10.1007\/3-540-45657-0_20"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"F. Copty, L. Fix, F. R, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking in an industrial setting. In Computer Aided Verification (CAV 2001), pages 436\u2013453, 2001.","DOI":"10.1007\/3-540-44585-4_43"},{"key":"2_CR8","unstructured":"S. German. Personal communication."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"S. G. Govindaraju and D. L. Dill. Counterexample-Guided choice of projections in approximate symbolic model checking. In IEEE International Conference on Computer Aided Design (ICCAD 2000), pages 115\u2013119, 2000.","DOI":"10.1109\/ICCAD.2000.896460"},{"key":"2_CR10","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1\u201333, Washington, D.C., 1990. IEEE Computer Society Press."},{"issue":"3","key":"2_CR11","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(3):291\u2013314, 2001.","journal-title":"Formal Methods in System Design"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-Aided-Verification of Coordinating Processes. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/papers , 2002.","DOI":"10.1007\/3-540-36577-X_2"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"M. W. Moskewicz, C. F. Madigan, Y. Z., L. Z., and S. Malik. Cha.: Engineering an efficient SAT solver. In Design Automation Conference, pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"A. P. O. Lichtenstein. Checking that finite state concurrent programs satisfy their linear specification. In POPL\u2019 85, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"2_CR16","unstructured":"J. K. S. S. H. V. Pankaj Chauhan, Ed Clarke and D. Wang. Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In Formal Methods in Computer Aided Design (FMCAD\u201902), November 2002."},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"D. Plaisted and S. Greenbaum. A structure preserving clause form translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"H. Sa\u00efdi and S. Graf. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Computer-Aided Verification, CAV\u2019 97, volume 1254, pages 72\u201383, Haifa, Israel, 1997. Springer-Verlag.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"2_CR19","unstructured":"J. P. M. Silva and K. A. Sakallah. GRASP-a new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, November 1996, 1996."},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"R. M. T. A. Henzinger, R. Jhala and G. Sutre. Lazy abstraction. In Principles of Programming Languages (POPL 2002), 2002.","DOI":"10.1145\/503272.503279"},{"key":"2_CR21","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic programverification. In Logic in Computer Science (LICS\u2019 86), pages 322\u2013331, 1986."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"D. Wang, P.-H. Ho, J. Long, J. H. Kukula, Y. Zhu, H.-K. 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":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:11:18Z","timestamp":1739992278000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}