{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T01:04:37Z","timestamp":1784768677507,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319997247","type":"print"},{"value":"9783319997254","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_25","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T13:45:50Z","timestamp":1535550350000},"page":"423-444","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction"],"prefix":"10.1007","author":[{"given":"Florian","family":"Zuleger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"issue":"1","key":"25_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2011.07.009","volume":"413","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142\u2013159 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15769-1_8"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-40018-9_9","volume-title":"Programming Languages and Systems","author":"H Anderson","year":"2003","unstructured":"Anderson, H., Khoo, S.-C.: Affine-based size-change termination. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 122\u2013140. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-40018-9_9"},{"key":"25_CR4","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3), 1\u201330 (2008)"},{"key":"25_CR5","unstructured":"Ben-Amram, A.M.: Monotonicity constraints for termination in the integer domain. Log. Methods Comput. Sci. 7(3), 1\u201343 (2011)"},{"issue":"3","key":"25_CR6","first-page":"18:1","volume":"9","author":"A Blass","year":"2008","unstructured":"Blass, A., Gurevich, Y.: Program termination and well partial orderings. ACM Trans. Comput. Log. 9(3), 18:1\u201318:26 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: VMCAI, pp. 88\u2013103 (2012)","DOI":"10.1007\/978-3-642-27940-9_7"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413\u2013429. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_28"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-16242-8_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Codish","year":"2010","unstructured":"Codish, M., Fuhs, C., Giesl, J., Schneider-Kamp, P.: Lazy abstraction for size-change termination. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 217\u2013232. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16242-8_16"},{"issue":"4\u20135","key":"25_CR10","first-page":"503","volume":"11","author":"M Codish","year":"2011","unstructured":"Codish, M., Gonopolskiy, I., Ben-Amram, A.M., Fuhs, C., Giesl, J.: Sat-based termination analysis using monotonicity constraints over the integers. TPLP 11(4\u20135), 503\u2013520 (2011)","journal-title":"TPLP"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-74240-1_20","volume-title":"Fundamentals of Computation Theory","author":"T Colcombet","year":"2007","unstructured":"Colcombet, T.: Factorisation forests for infinite words. In: Csuhaj-Varj\u00fa, E., \u00c9sik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 226\u2013237. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74240-1_20"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-662-44522-8_18","volume-title":"Mathematical Foundations of Computer Science 2014","author":"T Colcombet","year":"2014","unstructured":"Colcombet, T., Daviaud, L., Zuleger, F.: Size-change abstraction and max-plus automata. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 208\u2013219. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-44522-8_18"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-662-55751-8_1","volume-title":"Fundamentals of Computation Theory","author":"T Colcombet","year":"2017","unstructured":"Colcombet, T., Daviaud, L., Zuleger, F.: Automata and program analysis. In: Klasing, R., Zeitoun, M. (eds.) FCT 2017. LNCS, vol. 10472, pp. 3\u201310. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-55751-8_1"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-36742-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47\u201361. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_4"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-12736-1_15","volume-title":"Programming Languages and Systems","author":"A Flores-Montoya","year":"2014","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275\u2013295. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-12736-1_15"},{"issue":"1","key":"25_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with aprove. J. Autom. Reason. 58(1), 3\u201331 (2017)","journal-title":"J. Autom. Reason."},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292\u2013304 (2010)","DOI":"10.1145\/1806596.1806630"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Static Analysis","author":"M Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 22\u201350. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15769-1_4"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-73595-3_34","volume-title":"Automated Deduction \u2013 CADE-21","author":"A Krauss","year":"2007","unstructured":"Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460\u2013475. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73595-3_34"},{"issue":"3","key":"25_CR21","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/1498926.1498928","volume":"31","author":"CS Lee","year":"2009","unstructured":"Lee, C.S.: Ranking functions for size-change termination. ACM Trans. Program. Lang. Syst. 31(3), 10:1\u201310:42 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 401\u2013414. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11817963_36"},{"issue":"1","key":"25_CR24","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"3","key":"25_CR26","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1232420.1232422","volume":"29","author":"A Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), 15 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP, pp. 53\u201365 (2017)","DOI":"10.1145\/3018610.3018623"},{"issue":"1","key":"25_CR28","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0304-3975(90)90047-L","volume":"72","author":"I Simon","year":"1990","unstructured":"Simon, I.: Factorization forests of finite height. Theor. Comput. Sci. 72(1), 65\u201394 (1990)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reason."},{"issue":"12","key":"25_CR30","doi-asserted-by":"publisher","first-page":"1213","DOI":"10.1016\/j.apal.2016.06.001","volume":"167","author":"S Steila","year":"2016","unstructured":"Steila, S., Yokoyama, K.: Reverse mathematical bounds for the termination theorem. Ann. Pure Appl. Logic 167(12), 1213\u20131241 (2016)","journal-title":"Ann. Pure Appl. Logic"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Vidal, G.: Quasi-terminating logic programs for ensuring the termination of partial evaluation. In: PEPM, pp. 51\u201360 (2007)","DOI":"10.1145\/1244381.1244390"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-32347-8_17","volume-title":"Interactive Theorem Proving","author":"D Vytiniotis","year":"2012","unstructured":"Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full: adventures in constructive termination. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250\u2013265. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_17"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-319-20297-6_27","volume-title":"Computer Science \u2013 Theory and Applications","author":"F Zuleger","year":"2015","unstructured":"Zuleger, F.: Asymptotically precise ranking functions for deterministic size-change systems. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 426\u2013442. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-20297-6_27"},{"key":"25_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23702-7_22","volume-title":"Static Analysis","author":"F Zuleger","year":"2011","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280\u2013297. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23702-7_22"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T14:06:14Z","timestamp":1535551574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}