{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:44:44Z","timestamp":1725565484161},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_4","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"22-50","source":"Crossref","is-referenced-by-count":17,"title":["Size-Change Termination and Transition Invariants"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Heizmann","sequence":"first","affiliation":[]},{"given":"Neil D.","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Avery, J.: Size-change termination and bound analysis. In: Hagiya and Wadler [19], pp. 192\u2013207.","DOI":"10.1007\/11737414_14"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen and Stevens [25], pp. 158\u2013172","DOI":"10.1007\/3-540-46002-0_12"},{"key":"4_CR4","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"},{"issue":"3","key":"4_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1353445.1353450","volume":"30","author":"A.M. Ben-Amram","year":"2008","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst.\u00a030(3), 1\u201331 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"4_CR6","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s00236-008-0085-0","volume":"46","author":"A.M. Ben-Amram","year":"2009","unstructured":"Ben-Amram, A.M.: A complexity tradeoff in ranking-function termination proofs. Acta Informatica\u00a046(1), 57\u201372 (2009)","journal-title":"Acta Informatica"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. Logical Methods in Computer Science (2010)","DOI":"10.2168\/LMCS-6(3:2)2010"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Codish, M.: A SAT-based approach to size change termination with global ranking functions. In: Ramakrishnan and Rehof [33], pp. 218\u2013232","DOI":"10.1007\/978-3-540-78800-3_16"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Program termination analysis in polynomial time. ACM Trans. Program. Lang. Syst.\u00a029(1) (2007)","DOI":"10.1145\/1180475.1180480"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Ranking functions for size-change termination II. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:8)2009"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: Hofmann and Felleisen [22], pp. 211\u2013224","DOI":"10.1145\/1190216.1190249"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Abstraction, Reformulation, and Approximation","year":"2000","unstructured":"Choueiry, B.Y., Walsh, T. (eds.): SARA 2000. LNCS, vol.\u00a01864. Springer, Heidelberg (2000)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/11562931_25","volume-title":"Logic Programming","author":"M. Codish","year":"2005","unstructured":"Codish, M., Lagoon, V., Stuckey, P.J.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 326\u2013340. Springer, Heidelberg (2005)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach and Ball [35], pp. 415\u2013426","DOI":"10.1145\/1133981.1134029"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: No return! Journal of Formal Methods in System Design (2010)","DOI":"10.1007\/s10703-009-0087-8"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking. In: Choueiry and Walsh [12], pp. 1\u201325","DOI":"10.1007\/3-540-44914-0_1"},{"issue":"6","key":"4_CR17","doi-asserted-by":"publisher","first-page":"1147","DOI":"10.1145\/1108970.1108973","volume":"27","author":"A.J. Glenstrup","year":"2005","unstructured":"Glenstrup, A.J., Jones, N.D.: Termination analysis and specialization-point insertion in offline partial evaluation. ACM Trans. Program. Lang. Syst.\u00a027(6), 1147\u20131215 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR18","first-page":"16","volume-title":"POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A. Gotsman","year":"2009","unstructured":"Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 16\u201328. ACM, New York (2009)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Functional and Logic Programming","year":"2006","unstructured":"Hagiya, M., Wadler, P. (eds.): FLOPS 2006. LNCS, vol.\u00a03945. Springer, Heidelberg (2006)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants (online version) (2010), http:\/\/swt.informatik.uni-freiburg.de\/staff\/heizmann\/SCTandTI.pdf","DOI":"10.1007\/978-3-642-15769-1_4"},{"volume-title":"Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007","year":"2007","key":"4_CR21","unstructured":"Hinze, R., Ramsey, N. (eds.): Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, 2007, October 1-3. ACM Press, New York (2007)"},{"volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007","year":"2007","key":"4_CR22","unstructured":"Hofmann, M., Felleisen, M. (eds.): Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19. ACM, New York (2007)"},{"key":"4_CR23","volume-title":"Foundations of Computing","author":"N.D. Jones","year":"1997","unstructured":"Jones, N.D.: Computability and Complexity from a Programming Perspective. In: Foundations of Computing, 1st edn., MIT Press, Boston (1997)","edition":"1"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Bohr, N.: Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science\u00a04(1) (2008)","DOI":"10.2168\/LMCS-4(1:3)2008"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2002","unstructured":"Katoen, J.-P., Stevens, P. (eds.): TACAS 2002. LNCS, vol.\u00a02280. Springer, Heidelberg (2002)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/360204.360210","volume-title":"POPL 2001: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","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 2001: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.\u00a028, pp. 81\u201392. ACM Press, New York (2001)"},{"key":"4_CR28","volume-title":"Temporal verification of reactive systems: safety","author":"Z. Mannaand","year":"1995","unstructured":"Mannaand, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Heidelberg (1995)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"The Essence of Computation; Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones","year":"2002","unstructured":"Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.): The Essence of Computation; Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. LNCS, vol.\u00a02566. Springer, Heidelberg (2002)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen and Levi [38], pp. 239\u2013251","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"4_CR31","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/LICS.2004.1319598","volume-title":"LICS 2004: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, pp. 32\u201341. IEEE Computer Society, Los Alamitos (2004)"},{"key":"4_CR32","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1145\/1040305.1040317","volume-title":"POPL 20505: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL 20505: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.\u00a032, pp. 132\u2013144. ACM, New York (2005)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2008","unstructured":"Ramakrishnan, C.R., Rehof, J. (eds.): TACAS 2008. LNCS, vol.\u00a04963. Springer, Heidelberg (2008)"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-22","year":"2009","unstructured":"Schmidt, R.A. (ed.): CADE-22. LNCS, vol.\u00a05663. Springer, Heidelberg (2009)"},{"volume-title":"Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation","year":"2006","key":"4_CR35","unstructured":"Schwartzbach, M.I., Ball, T. (eds.): Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14. ACM, New York (2006)"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: Hinze and Ramsey [21], pp. 71\u201384","DOI":"10.1145\/1291151.1291165"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Sereni, D., Jones, N.D.: Termination analysis of higher-order functional programs. In: Yi [40], pp. 281\u2013297","DOI":"10.1007\/11575467_19"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","year":"2004","unstructured":"Steffen, B., Levi, G. (eds.): VMCAI 2004. LNCS, vol.\u00a02937. Springer, Heidelberg (2004)"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Swiderski, S., Parting, M., Giesl, J., Fuhs, C., Schneider-Kamp, P.: Termination analysis by dependency pairs and inductive theorem proving. In Schmidt [34], pp.322\u2013338","DOI":"10.1007\/978-3-642-02959-2_25"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","year":"2005","unstructured":"Yi, K. (ed.): APLAS 2005. LNCS, vol.\u00a03780. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T07:58:35Z","timestamp":1685779115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}