{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:31:19Z","timestamp":1764873079713},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642137532"},{"type":"electronic","value":"9783642137549"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13754-9_4","type":"book-chapter","created":{"date-parts":[[2010,6,30]],"date-time":"2010-06-30T11:05:52Z","timestamp":1277895952000},"page":"61-71","source":"Crossref","is-referenced-by-count":7,"title":["The Localization Reduction and Counterexample-Guided Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-56496-9_12","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1993","unstructured":"Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing Verification by Successive Approximation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 137\u2013150. Springer, Heidelberg (1993); Also Inf. Comput.\u00a0118(1), 142\u2013157 (1995)"},{"key":"4_CR2","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":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-540-71209-1_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2007","unstructured":"Amla, N., McMillan, K.L.: Combining Abstraction Refinement and SAT-Based Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 405\u2013419. Springer, Heidelberg (2007)"},{"key":"4_CR4","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.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"4_CR6","first-page":"385","volume-title":"ICSE","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in c. In: ICSE, pp. 385\u2013395. IEEE Computer Society, Los Alamitos (2003)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","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.M., Kukula, J.H., 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, pp. 33\u201351. Springer, Heidelberg (2002)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"5","key":"4_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"4_CR10","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.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Gupta, A., Kukula, J.H., 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)"},{"issue":"5","key":"4_CR11","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst.\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR12","unstructured":"Chaki, S.: A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs. PhD Thesis, Carnegie Mellon University (2005)"},{"key":"4_CR13","first-page":"19","volume-title":"LICS","author":"E.M. Clarke","year":"2002","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: LICS, pp. 19\u201329. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Satabs: Sat-based predicate abstraction for ansi-c. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-540-39910-0_9","volume-title":"Verification: Theory and Practice","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 208\u2013224. Springer, Heidelberg (2004)"},{"key":"4_CR17","first-page":"51","volume-title":"LICS 2001","author":"S. Das","year":"2001","unstructured":"Das, S., Dill, D.L.: Successive Approximation of Abstract Transition Relations. In: LICS 2001, pp. 51\u201358. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"4_CR18","unstructured":"Lucent\u2019s Bell Introduces FormalCheck. Electronic News (April 1997)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, p. 356. Springer, Heidelberg (2001)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u0131di, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"key":"4_CR22","volume-title":"POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL. ACM, New York (2004)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 39\u201351. Springer, Heidelberg (2005)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv.\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"4_CR26","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"issue":"5","key":"4_CR27","first-page":"534","volume":"47","author":"R.P. Kurshan","year":"2000","unstructured":"Kurshan, R.P.: Program Verification. Notices of the AMS\u00a047(5), 534\u2013545 (2000)","journal-title":"Notices of the AMS"},{"key":"4_CR28","unstructured":"Lu, Y.: Automated Abstraction in Model Checking. PhD Thesis, Carnegie Mellon University (2000)"},{"key":"4_CR29","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.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10722167_1","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2000","unstructured":"Pnueli, A.: Keynote address: Abstraction, composition, symmetry, and a little deduction: The remedies to state explosion. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, p. 1. Springer, Heidelberg (2000)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31980-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2005","unstructured":"Pnueli, A., Podelski, A., Rybalchenko, A.: Separating fairness and well-foundedness for the analysis of fair discrete systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 124\u2013139. Springer, Heidelberg (2005)"},{"key":"4_CR33","first-page":"32","volume-title":"LICS","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society, Los Alamitos (2004)"},{"key":"4_CR34","first-page":"953","volume-title":"Principles of Operations Research","author":"H.M. Wagner","year":"1975","unstructured":"Wagner, H.M.: Principles of Operations Research, pp. 953\u2013958. Prentice Hall, Englewood Cliffs (1975); see Appendix I: Advanced Topics in Network Algorithms"}],"container-title":["Lecture Notes in Computer Science","Time for Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13754-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,19]],"date-time":"2019-01-19T14:03:39Z","timestamp":1547906619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13754-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642137532","9783642137549"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13754-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}