{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:30:25Z","timestamp":1762101025158},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540272311"},{"type":"electronic","value":"9783540316862"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_11","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T08:33:28Z","timestamp":1268382808000},"page":"112-124","source":"Crossref","is-referenced-by-count":17,"title":["Abstraction Refinement for Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Anubhav","family":"Gupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-30494-4_19","volume-title":"Formal Methods in Computer-Aided Design","author":"N. Amla","year":"2004","unstructured":"Amla, N., McMillan, K.L.: A hybrid of counterexample-based and proof-based abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-45657-0_6","volume-title":"Computer Aided Verification","author":"S. Barner","year":"2002","unstructured":"Barner, S., Geist, D., Gringauze, A.: Symbolic localization reduction with reconstruction layering and backtracking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 65. Springer, Heidelberg (2002)"},{"key":"11_CR4","first-page":"21","volume-title":"Proceedings of the Eleventh National Conference on Artificial Intelligence","author":"J.M. Crawford","year":"1993","unstructured":"Crawford, J.M., Anton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Proceedings of the Eleventh National Conference on Artificial Intelligence, pp. 21\u201327. AAAI Press, Menlo Park (1993)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_3","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Chauhan","year":"2002","unstructured":"Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45657-0_20","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2002","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 265\u2013279. Springer, Heidelberg (2002)"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M.K., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based bmc with proof analysis. In: ICCAD, pp. 416\u2013423 (2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-36577-X_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Glusman","year":"2003","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 176\u2013191. Springer, Heidelberg (2003)"},{"key":"11_CR10","volume-title":"Computer aided verification of coordinating processes","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R.: Computer aided verification of coordinating processes. Princeton University Press, Princeton (1994)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. McMillan","year":"2003","unstructured":"McMillan, K., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"11_CR12","unstructured":"McMillan, K.: From bounded to unbounded model checking (2003)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. Design Automation Conference 2001, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"11_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48159-1_5","volume-title":"Progress in Artificial Intelligence","author":"J.P.M. Silva","year":"1999","unstructured":"Silva, J.P.M.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol.\u00a01695, pp. 62\u201374. Springer, Heidelberg (1999)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Wang, C., Jin, H., Hachtel, G.D., Somenzi, F.: Refining the SAT decision ordering for bounded model checking. In: ACM\/IEEE 41th Design Automation Conference (DAC 2004), pp. 535\u2013538 (2004)","DOI":"10.1145\/996566.996713"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:04:57Z","timestamp":1605625497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11513988_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}