{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:46:22Z","timestamp":1770295582166,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540285847","type":"print"},{"value":"9783540319719","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11547662_8","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:36:20Z","timestamp":1127831780000},"page":"87-101","source":"Crossref","is-referenced-by-count":76,"title":["Abstraction Refinement for Termination"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: FMICS 2002: Formal Methods for Industrial Critical Systems. ENTCS, vol.\u00a066(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003: Int. Conf. on Software Engineering, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"8_CR6","volume-title":"Model checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"8_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44914-0_1","volume-title":"Abstraction, Reformulation, and Approximation","author":"P. Cousot","year":"2000","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol.\u00a01864, pp. 1\u201315. Springer, Heidelberg (2000)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"8_CR11","first-page":"238","volume-title":"POPL 1977: Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"8_CR12","first-page":"84","volume-title":"POPL 1978: Principles of Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978: Principles of Programming Languages, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"8_CR13","first-page":"51","volume-title":"LICS 2001: Logic in Computer Science","author":"S. Das","year":"2001","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: LICS 2001: Logic in Computer Science, pp. 51\u201360. IEEE, Los Alamitos (2001)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44685-0_5","volume-title":"CONCUR 2001 - Concurrency Theory","author":"J. Hatcliff","year":"2001","unstructured":"Hatcliff, J., Dwyer, M.B.: Using the bandera tool set to model-check properties of concurrent java software. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 39\u201358. Springer, Heidelberg (2001)"},{"key":"8_CR15","first-page":"232","volume-title":"POPL 2004: Principles of Programming Languages","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004: Principles of Programming Languages, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Jain, H., Gupta, A., Ganai, M.K.: Localization and register sharing for predicate abstraction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 397\u2013412. Springer, Heidelberg (2005) (to appear)","DOI":"10.1007\/978-3-540-31980-1_26"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Lakhnech","year":"2001","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 98\u2013112. Springer, Heidelberg (2001)"},{"key":"8_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer, Heidelberg (1995)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 139\u2013153. Springer, Heidelberg (2000)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"8_CR21","first-page":"32","volume-title":"LICS 2004: Logic in Computer Science","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004: Logic in Computer Science, pp. 32\u201341. IEEE, Los Alamitos (2004)"},{"key":"8_CR22","first-page":"132","volume-title":"POPL 2005: Principles of Programming Languages","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL 2005: Principles of Programming Languages, pp. 132\u2013144. ACM Press, New York (2005)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-31987-0_8","volume-title":"Programming Languages and Systems","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Schaefer, I., Wagner, S.: Summaries for while programs with recursion. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 94\u2013107. Springer, Heidelberg (2005)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A. Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 70\u201382. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11547662_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:40:29Z","timestamp":1605642029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11547662_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540285847","9783540319719"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11547662_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}