{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:45:37Z","timestamp":1770277537142,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_9","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"89-103","source":"Crossref","is-referenced-by-count":60,"title":["Termination Analysis with Compositional Transition Invariants"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133981.1134029","volume-title":"PLDI","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426. ACM, New York (2006)"},{"key":"9_CR2","first-page":"236","volume-title":"TACAS","author":"B. Cook","year":"2010","unstructured":"Cook, B., Kroening, D., Ruemmer, P., Wintersteiger, C.: Ranking function synthesis for bit-vector relations. In: TACAS, pp. 236\u2013250. Springer, Heidelberg (2010)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society, Los Alamitos (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"9_CR4","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":"9_CR5","series-title":"Lecture Notes in Computer Science","first-page":"465","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. 465\u2013486. Springer, Heidelberg (2004)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/53990.53994","volume-title":"PLDI","author":"S. Horwitz","year":"1988","unstructured":"Horwitz, S., Reps, T.W., Binkley, D.: Interprocedural slicing using dependence graphs. In: PLDI, pp. 35\u201346. ACM, New York (1988)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-88387-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 111\u2013125. Springer, Heidelberg (2008)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR12","first-page":"230","volume":"2","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc.\u00a02, 230\u2013265 (1936)","journal-title":"Proc. London Math. Soc."},{"key":"9_CR13","unstructured":"Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67\u201369 (1949)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BFb0027001","volume-title":"Algebraic and Logic Programming","author":"M. Codish","year":"1997","unstructured":"Codish, M., Taboch, C.: A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP 1997 and HOA 1997. LNCS, vol.\u00a01298, pp. 31\u201345. Springer, Heidelberg (1997)"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Appl. Alg. in Eng., Comm. & Comp.\u00a016, 229\u2013270 (2005)","journal-title":"Appl. Alg. in Eng., Comm. & Comp."},{"key":"9_CR16","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/360204.360210","volume-title":"POPL","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392. ACM, New York (2001)"},{"key":"9_CR17","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":"9_CR18","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":"9_CR19","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/1190215.1190249","volume":"42","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. SIGPLAN Not.\u00a042, 211\u2013224 (2007)","journal-title":"SIGPLAN Not."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci.\u00a066 (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T05:01:10Z","timestamp":1711602070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}