{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:42Z","timestamp":1751660502797},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,1]]},"abstract":"<jats:p>A<jats:italic>size-change termination algorithm<\/jats:italic>takes as input abstract information about a program in the form of<jats:italic>size-change graphs<\/jats:italic>and uses it to determine whether any infinite computation would imply that some data decrease in size infinitely. Since such an infinite descent is presumed impossible, this proves program termination. The property of the graphs that implies program termination is called SCT. There are many examples of practical programs whose termination can be verified by creating size-change graphs and testing them for SCT.The size-change graph abstraction is useful because the graphs often carry sufficient information to deduce termination, and at the same time are simple enough to be analyzed automatically. However, there is a tradeoff between the completeness and efficiency of this analysis, and complete algorithms in the literature can easily be pushed to an exponential combinatorial search by certain patterns in the graph structures.We therefore propose a novel algorithm to detect common forms of parameter-descent behavior efficiently. Specifically, we target lexicographic descent, multiset descent, and min- and max-descent. Our algorithm makes it possible to verify practical instances of SCT while guarding against unwarranted combinatorial search. It has worst-case time complexity cubic in the input size, and its effectiveness is demonstrated empirically using a test suite of over 90 programs.<\/jats:p>","DOI":"10.1145\/1180475.1180480","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T19:20:08Z","timestamp":1175800808000},"page":"1-37","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Program termination analysis in polynomial time"],"prefix":"10.1145","volume":"29","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[{"name":"The Academic College of Tel-Aviv-Yaffo, Tel-Aviv, Israel"}]},{"given":"Chin Soon","family":"Lee","sequence":"additional","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany"}]}],"member":"320","published-online":{"date-parts":[[2007,1]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 1st Asian Symposium on Programming Languages and Systems (APLAS), A. Ohori, Ed. Lecture Notes in Computer Science","volume":"2895","author":"Anderson H."},{"key":"e_1_2_1_2_1","volume-title":"Tech. Rep. TRB6\/05","author":"Anderson H.","year":"2005"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Apt K. R. and Pedreschi D. 1994. Modular termination proofs for logic and pure Prolog programs. In Advances in Logic Programming Theory. Oxford University Press 183--229. Apt K. R. and Pedreschi D. 1994. Modular termination proofs for logic and pure Prolog programs. In Advances in Logic Programming Theory. Oxford University Press 183--229.","DOI":"10.1093\/oso\/9780198538530.003.0004"},{"key":"e_1_2_1_4_1","unstructured":"Arts T. 2001. Automatically proving termination and innermost normalisation of term rewriting systems. Ph.D. thesis Universiteit Utrecht The Netherlands. Arts T. 2001. Automatically proving termination and innermost normalisation of term rewriting systems. Ph.D. thesis Universiteit Utrecht The Netherlands."},{"key":"e_1_2_1_6_1","series-title":"Lecture Notes in Computer Science","volume-title":"The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen et al. Eds","author":"Ben-Amram A."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS). MIT Press","author":"Bueno F."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562931_25"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(99)00079-5"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP), M. Hanus et al., Eds. Lecture Notes in Computer Science","volume":"1298","author":"Codish M."},{"key":"e_1_2_1_11_1","unstructured":"Cormen T. H. Leiserson C. E. and Rivest R. L. 2001. Introduction to Algorithms. MIT Press Cambridge MA. Cormen T. H. Leiserson C. E. and Rivest R. L. 2001. Introduction to Algorithms. MIT Press Cambridge MA."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"De Schreye D. and Decorte S. 1994. Termination of logic programs: The never-ending story. J. Logic Program. 19--20 199--260. De Schreye D. and Decorte S. 1994. Termination of logic programs: The never-ending story. J. Logic Program. 19--20 199--260.","DOI":"10.1016\/0743-1066(94)90027-2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI). Springer Verlag.","author":"Genaim S."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science","volume":"3091","author":"Giesl J."},{"key":"e_1_2_1_18_1","volume-title":"Tech. Rep. D-498","author":"Glenstrup A.","year":"2004"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science","volume":"3091","author":"Jones N. D."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010004307057"},{"key":"e_1_2_1_21_1","unstructured":"Lee C. S. 2001. Program termination analysis and termination of offline partial evaluation. Ph.D. thesis UWA Australia. Lee C. S. 2001. Program termination analysis and termination of offline partial evaluation. Ph.D. thesis UWA Australia."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645435.652648"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Lindenstrauss N. and Sagiv Y. 1997a. Automatic termination analysis of logic programs (with detailed experimental results). http:\/\/www.cs.huji.ac.il\/~naomil\/. Lindenstrauss N. and Sagiv Y. 1997a. Automatic termination analysis of logic programs (with detailed experimental results). http:\/\/www.cs.huji.ac.il\/~naomil\/.","DOI":"10.7551\/mitpress\/4299.003.0011"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 14th International Conference on Logic Programming (ICLP), L. Naish, Ed. MIT Press","author":"Lindenstrauss N."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263762"},{"key":"e_1_2_1_27_1","unstructured":"P\u00e9ter R. 1967. Recursive Functions. Academic Press. P\u00e9ter R. 1967. Recursive Functions. Academic Press."},{"key":"e_1_2_1_28_1","volume-title":"Lecture Notes in Artificial Intelligence","volume":"446","author":"Pl\u00fcmer L.","year":"1990"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040317"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS), V. Saraswat and K. Ueda, Eds. MIT Press","author":"Sagiv Y.","year":"1991"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science","volume":"2706","author":"Thiemann R."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-005-0179-7"},{"key":"e_1_2_1_33_1","volume-title":"Reprinted in The Early British Computer Conferences","volume":"14","author":"Turing A. M.","year":"1948"},{"key":"e_1_2_1_34_1","unstructured":"Wahlstedt D. 2000. Detecting termination using size-change in parameter values. Master's thesis G\u00f6teborgs Universitet Sweden. Wahlstedt D. 2000. Detecting termination using size-change in parameter values. Master's thesis G\u00f6teborgs Universitet Sweden."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1180475.1180480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,12]],"date-time":"2024-02-12T23:59:00Z","timestamp":1707782340000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1180475.1180480"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,1]]}},"alternative-id":["10.1145\/1180475.1180480"],"URL":"https:\/\/doi.org\/10.1145\/1180475.1180480","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1]]},"assertion":[{"value":"2007-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}