{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T05:28:28Z","timestamp":1738992508780,"version":"3.37.0"},"reference-count":103,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,3]]},"abstract":"\n It is important to prove that supposedly terminating programs actually terminate, particularly if those programs must be run on critical systems or downloaded into a client such as a mobile phone. Although termination of computer programs is generally undecidable, it is possible and useful to prove termination of a large, nontrivial subset of the terminating programs. In this article, we present our termination analyzer for sequential Java bytecode, based on a program property called\n path-length<\/jats:italic>\n . We describe the analyses which are needed before the path-length can be computed such as sharing, cyclicity, and aliasing. Then we formally define the path-length analysis and prove it correct with respect to a reference denotational semantics of the bytecode. We show that a constraint logic program\n P<\/jats:italic>\n \n CLP<\/jats:italic>\n <\/jats:sub>\n can be built from the result of the path-length analysis of a Java bytecode program\n P<\/jats:italic>\n and formally prove that if\n P<\/jats:italic>\n \n CLP<\/jats:italic>\n <\/jats:sub>\n terminates, then\n P<\/jats:italic>\n also terminates. Hence a termination prover for constraint logic programs can be applied to prove the termination of\n P<\/jats:italic>\n . We conclude with some discussion of the possibilities and limitations of our approach. Ours is the first existing termination analyzer for Java bytecode dealing with any kind of data structures dynamically allocated on the heap and which does not require any help or annotation on the part of the user.\n <\/jats:p>","DOI":"10.1145\/1709093.1709095","type":"journal-article","created":{"date-parts":[[2010,3,16]],"date-time":"2010-03-16T19:25:36Z","timestamp":1268767536000},"page":"1-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":84,"title":["A termination analyzer for Java bytecode based on path-length"],"prefix":"10.1145","volume":"32","author":[{"given":"Fausto","family":"Spoto","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Verona, Italy"}]},{"given":"Fred","family":"Mesnard","sequence":"additional","affiliation":[{"name":"IREMIA, LIM, Universit\u00e9 de la R\u00e9union, France"}]},{"given":"\u00c9tienne","family":"Payet","sequence":"additional","affiliation":[{"name":"IREMIA, LIM, Universit\u00e9 de la R\u00e9union, France"}]}],"member":"320","published-online":{"date-parts":[[2010,3]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Aho A. V. Sethi R. and Ullman J. D. 1986. Compilers Principles Techniques and Tools. Addison Wesley.","key":"e_1_2_2_1_1","DOI":"10.5555\/6448"},{"doi-asserted-by":"publisher","key":"e_1_2_2_2_1","DOI":"10.1007\/s10270-004-0058-x"},{"doi-asserted-by":"publisher","key":"e_1_2_2_3_1","DOI":"10.1007\/978-3-540-68863-1_2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_4_1","DOI":"10.1007\/978-3-540-68863-1_2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_5_1","DOI":"10.5555\/1762174.1762191"},{"doi-asserted-by":"publisher","key":"e_1_2_2_6_1","DOI":"10.1007\/11737414_14"},{"doi-asserted-by":"publisher","key":"e_1_2_2_7_1","DOI":"10.1109\/SEFM.2007.32"},{"doi-asserted-by":"publisher","key":"e_1_2_2_8_1","DOI":"10.1145\/236338.236371"},{"doi-asserted-by":"publisher","key":"e_1_2_2_9_1","DOI":"10.1016\/j.scico.2005.02.003"},{"doi-asserted-by":"publisher","key":"e_1_2_2_10_1","DOI":"10.1016\/j.scico.2007.08.001"},{"doi-asserted-by":"publisher","key":"e_1_2_2_11_1","DOI":"10.1016\/j.entcs.2005.02.026"},{"doi-asserted-by":"publisher","key":"e_1_2_2_12_1","DOI":"10.1007\/11804192_17"},{"doi-asserted-by":"publisher","key":"e_1_2_2_13_1","DOI":"10.1145\/1180475.1180480"},{"doi-asserted-by":"publisher","key":"e_1_2_2_14_1","DOI":"10.5555\/1770351.1770381"},{"doi-asserted-by":"publisher","key":"e_1_2_2_15_1","DOI":"10.1145\/1190216.1190249"},{"doi-asserted-by":"publisher","key":"e_1_2_2_16_1","DOI":"10.1007\/11817963_35"},{"doi-asserted-by":"publisher","key":"e_1_2_2_17_1","DOI":"10.1007\/11817963_47"},{"doi-asserted-by":"publisher","key":"e_1_2_2_18_1","DOI":"10.1007\/978-3-540-30579-8_8"},{"doi-asserted-by":"publisher","key":"e_1_2_2_19_1","DOI":"10.1145\/73721.73741"},{"doi-asserted-by":"publisher","key":"e_1_2_2_20_1","DOI":"10.1145\/1328438.1328453"},{"doi-asserted-by":"publisher","key":"e_1_2_2_21_1","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"publisher","key":"e_1_2_2_22_1","DOI":"10.1007\/978-3-540-30579-8_11"},{"doi-asserted-by":"publisher","key":"e_1_2_2_23_1","DOI":"10.1145\/158511.158639"},{"key":"e_1_2_2_24_1","volume-title":"Proceedings of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07)","volume":"4915","author":"Codish M.","year":"2007","unstructured":"Codish, M. 2007. Proving termination with (boolean) satisfaction. In Proceedings of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07). A. King, Ed. Lecture Notes in Computer Science, vol. 4915. 1--7."},{"doi-asserted-by":"publisher","key":"e_1_2_2_25_1","DOI":"10.1007\/11562931_25"},{"doi-asserted-by":"publisher","key":"e_1_2_2_26_1","DOI":"10.1016\/S0743-1066(99)00006-0"},{"doi-asserted-by":"publisher","key":"e_1_2_2_27_1","DOI":"10.1007\/11547662_8"},{"doi-asserted-by":"publisher","key":"e_1_2_2_28_1","DOI":"10.1145\/1133981.1134029"},{"doi-asserted-by":"publisher","key":"e_1_2_2_29_1","DOI":"10.1007\/11817963_37"},{"doi-asserted-by":"publisher","key":"e_1_2_2_30_1","DOI":"10.1145\/1250734.1250771"},{"doi-asserted-by":"publisher","key":"e_1_2_2_31_1","DOI":"10.1145\/337180.337234"},{"doi-asserted-by":"publisher","key":"e_1_2_2_32_1","DOI":"10.1007\/978-3-540-30579-8_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_33_1","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_2_2_34_1","DOI":"10.1145\/567752.567778"},{"doi-asserted-by":"publisher","key":"e_1_2_2_35_1","DOI":"10.1145\/512760.512770"},{"doi-asserted-by":"publisher","key":"e_1_2_2_36_1","DOI":"10.1016\/0743-1066(94)90027-2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_37_1","DOI":"10.5555\/646153.679523"},{"doi-asserted-by":"publisher","key":"e_1_2_2_38_1","DOI":"10.1007\/s002000100065"},{"doi-asserted-by":"publisher","key":"e_1_2_2_39_1","DOI":"10.1007\/11691372_19"},{"volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R. W.","unstructured":"Floyd, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, J. T. Schwartz, Ed. Proceedings of Symposia in Applied Mathematics, vol. 19. American Mathematical Society, Providence, Rhode Island, 19--32.","key":"e_1_2_2_40_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_41_1","DOI":"10.1145\/326619.326789"},{"doi-asserted-by":"publisher","key":"e_1_2_2_42_1","DOI":"10.1017\/S1471068404002236"},{"volume-title":"Proceedings of the 10th Workshop on Formal Techniques for Java-like Programs (FTfJP'08)","author":"Genaim S.","unstructured":"Genaim, S. and Spoto, F. 2008. Constancy analysis. In Proceedings of the 10th Workshop on Formal Techniques for Java-like Programs (FTfJP'08), M. Huisman, Ed.","key":"e_1_2_2_43_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_44_1","DOI":"10.1007\/11814771_24"},{"doi-asserted-by":"publisher","key":"e_1_2_2_45_1","DOI":"10.1007\/11823230_16"},{"doi-asserted-by":"publisher","key":"e_1_2_2_46_1","DOI":"10.1145\/360204.375719"},{"doi-asserted-by":"publisher","key":"e_1_2_2_47_1","DOI":"10.1016\/0743-1066(94)90033-7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_48_1","DOI":"10.1145\/1146809.1146811"},{"doi-asserted-by":"publisher","key":"e_1_2_2_49_1","DOI":"10.1007\/s00165-007-0026-7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_50_1","DOI":"10.1145\/360204.360210"},{"doi-asserted-by":"publisher","key":"e_1_2_2_51_1","DOI":"10.1016\/j.entcs.2007.02.059"},{"key":"e_1_2_2_52_1","volume-title":"Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP'04)","volume":"3086","author":"Leino K. R. M.","unstructured":"Leino, K. R. M. and M\u00fcller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP'04). M. Odersky, Ed. Lecture Notes in Computer Science, vol. 3086. Springer, 491--516."},{"doi-asserted-by":"publisher","key":"e_1_2_2_53_1","DOI":"10.1007\/11526841_4"},{"doi-asserted-by":"publisher","key":"e_1_2_2_54_1","DOI":"10.1145\/1342211.1342225"},{"doi-asserted-by":"publisher","key":"e_1_2_2_55_1","DOI":"10.5555\/647766.736024"},{"doi-asserted-by":"publisher","unstructured":"Lindholm T. and Yellin F. 1999. The Java#8482; Virtual Machine Specification 2nd ed. Addison-Wesley.","key":"e_1_2_2_56_1","DOI":"10.5555\/553607"},{"doi-asserted-by":"publisher","key":"e_1_2_2_57_1","DOI":"10.1007\/11562948_33"},{"doi-asserted-by":"crossref","unstructured":"Loginov A. Reps T. W. and Sagiv M. 2006. Refinement-based verification for possibly-cyclic lists. In Proceedings of Theory and Practice of Program Analysis and Compilation Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday T. W. Reps M. Sagiv and J. Bauer Eds. Lecture Notes in Computer Science vol. 4444. Springer 247--272.","key":"e_1_2_2_58_1","DOI":"10.1007\/978-3-540-71322-7_12"},{"doi-asserted-by":"publisher","key":"e_1_2_2_59_1","DOI":"10.5555\/1788374.1788393"},{"doi-asserted-by":"publisher","key":"e_1_2_2_60_1","DOI":"10.1145\/1134285.1134438"},{"doi-asserted-by":"publisher","key":"e_1_2_2_61_1","DOI":"10.1007\/11817963_36"},{"doi-asserted-by":"publisher","key":"e_1_2_2_62_1","DOI":"10.1145\/376656.376806"},{"doi-asserted-by":"publisher","key":"e_1_2_2_63_1","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_2_64_1","volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming, M. Maher, Ed. The MIT Press, 7--21","author":"Mesnard F.","year":"1996","unstructured":"Mesnard, F. 1996. Inferring left-terminating classes of queries for constraint logic programs. In Proceedings of the Joint International Conference and Symposium on Logic Programming, M. Maher, Ed. The MIT Press, 7--21."},{"doi-asserted-by":"publisher","key":"e_1_2_2_65_1","DOI":"10.1017\/S1471068404002017"},{"doi-asserted-by":"publisher","key":"e_1_2_2_66_1","DOI":"10.1017\/S1471068407003122"},{"doi-asserted-by":"publisher","key":"e_1_2_2_67_1","DOI":"10.1007\/s10990-006-8609-1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_68_1","DOI":"10.1145\/1353445.1353446"},{"key":"e_1_2_2_69_1","volume-title":"Proceedings of the Workshop on Verified Software: Theories, Tools, Experiments (VSTTE'07)","volume":"4171","author":"M\u00fcller P.","year":"2007","unstructured":"M\u00fcller, P. 2007. Reasoning about object structures using ownership. In Proceedings of the Workshop on Verified Software: Theories, Tools, Experiments (VSTTE'07). B. Meyer and J. Woodcock, Eds. Lecture Notes in Computer Science, vol. 4171. Springer."},{"key":"e_1_2_2_70_1","volume-title":"Proceedings of the 21st International Conference on Logic Programming (ICLP'05)","volume":"3668","author":"Nyugen M. T.","unstructured":"Nyugen, M. T. and De Schreye, D. 2005. Polynomial interpretations as a basis for termination analysis of logic programs. In Proceedings of the 21st International Conference on Logic Programming (ICLP'05). M. Gabbrielli and G. Gupta, Eds. Lecture Notes in Computer Science, vol. 3668. Springer, 311--326."},{"doi-asserted-by":"publisher","key":"e_1_2_2_71_1","DOI":"10.5555\/647199.718692"},{"doi-asserted-by":"publisher","key":"e_1_2_2_72_1","DOI":"10.1145\/118014.117965"},{"doi-asserted-by":"publisher","key":"e_1_2_2_73_1","DOI":"10.5555\/2391451.2391481"},{"doi-asserted-by":"publisher","key":"e_1_2_2_74_1","DOI":"10.1145\/244795.244798"},{"doi-asserted-by":"publisher","key":"e_1_2_2_75_1","DOI":"10.5555\/92069"},{"key":"e_1_2_2_76_1","volume-title":"Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04)","volume":"2937","author":"Podelski A.","unstructured":"Podelski, A. and Rybalchenko, A. 2004a. A complete method for synthesis of linear ranking functions. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04). B. Steffen and G. Levi, Eds. Lecture Notes in Computer Science, vol. 2937. Springer, 239--251."},{"doi-asserted-by":"publisher","key":"e_1_2_2_77_1","DOI":"10.5555\/1018438.1021840"},{"doi-asserted-by":"publisher","key":"e_1_2_2_78_1","DOI":"10.1145\/1232420.1232422"},{"doi-asserted-by":"publisher","key":"e_1_2_2_79_1","DOI":"10.5555\/646158.679877"},{"key":"e_1_2_2_80_1","volume-title":"Proceedings of Millennial Perspectives in Computer Science, Symposium in Honour of Sir Tony Hoare, J. Davies, B. Roscoe, and J. Woodcock, Eds. 303--321","author":"Reynolds J. C.","year":"2000","unstructured":"Reynolds, J. C. 2000. Intuitionistic reasoning about shared mutable data structure. In Proceedings of Millennial Perspectives in Computer Science, Symposium in Honour of Sir Tony Hoare, J. Davies, B. Roscoe, and J. Woodcock, Eds. 303--321."},{"doi-asserted-by":"publisher","key":"e_1_2_2_81_1","DOI":"10.1007\/11609773_7"},{"doi-asserted-by":"publisher","key":"e_1_2_2_82_1","DOI":"10.1007\/978-3-540-30579-8_14"},{"doi-asserted-by":"publisher","key":"e_1_2_2_83_1","DOI":"10.5555\/1759187.1759206"},{"doi-asserted-by":"publisher","key":"e_1_2_2_84_1","DOI":"10.1007\/11547662_22"},{"doi-asserted-by":"publisher","key":"e_1_2_2_85_1","DOI":"10.5555\/647171.718319"},{"unstructured":"Spoto F. 2008a. The julia static analyser. http:\/\/profs.sci.univr.it\/~spoto\/julia.","key":"e_1_2_2_86_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_87_1","DOI":"10.1109\/SEFM.2008.8"},{"volume-title":"International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)","author":"Spoto F.","unstructured":"Spoto, F., Hill, P. M., and Payet, E. 2006. Path-Length analysis for object-oriented programs. In International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06). http:\/\/profs.sci.univr.it\/~spoto\/papers.html.","key":"e_1_2_2_88_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_89_1","DOI":"10.1145\/937563.937565"},{"unstructured":"Spoto F. Mesnard F. and Payet E. 2008. Julia + BinTerm: An automatic termination prover for Java bytecode. http:\/\/spy.sci.univr.it\/JuliaWeb.","key":"e_1_2_2_90_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_91_1","DOI":"10.1016\/j.entcs.2009.11.019"},{"doi-asserted-by":"publisher","key":"e_1_2_2_92_1","DOI":"10.1145\/237721.237727"},{"doi-asserted-by":"crossref","unstructured":"Stoer J. and Witzgall C. 1970. Convexity and Optimization in Finite Dimensions I. Springer.","key":"e_1_2_2_93_1","DOI":"10.1007\/978-3-642-46216-0"},{"doi-asserted-by":"publisher","key":"e_1_2_2_94_1","DOI":"10.5555\/1770351.1770377"},{"doi-asserted-by":"publisher","key":"e_1_2_2_95_1","DOI":"10.1007\/978-3-540-31980-1_35"},{"unstructured":"Taboch C. Genaim S. and Codish M. TerminWeb: Semantic based termination analyser for logic programs. http:\/\/www.cs.bgu.ac.il\/~mcodish\/TerminWeb.","key":"e_1_2_2_96_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_97_1","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_98_1","first-page":"230","article-title":"On computable numbers, with an application to the entscheidungsproblem","volume":"42","author":"Turing A.","year":"1936","unstructured":"Turing, A. 1936. On computable numbers, with an application to the entscheidungsproblem. London Math. Soc. 42, 2, 230--265.","journal-title":"London Math. Soc."},{"doi-asserted-by":"publisher","key":"e_1_2_2_99_1","DOI":"10.1145\/42282.42285"},{"doi-asserted-by":"publisher","key":"e_1_2_2_100_1","DOI":"10.1023\/A:1022920129859"},{"doi-asserted-by":"publisher","key":"e_1_2_2_101_1","DOI":"10.1016\/j.entcs.2005.02.040"},{"doi-asserted-by":"publisher","key":"e_1_2_2_102_1","DOI":"10.1007\/978-3-540-31987-0_23"},{"doi-asserted-by":"crossref","unstructured":"Wilhelm R. Reps T. W. and Sagiv S. 2002. Shape analysis and applications. In The Compiler Design Handbook Y. N. Srikant and P. Shankar Eds. 175--218.","key":"e_1_2_2_103_1","DOI":"10.1201\/9781420040579.ch5"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1709093.1709095","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T18:47:37Z","timestamp":1738954057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1709093.1709095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":103,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["10.1145\/1709093.1709095"],"URL":"https:\/\/doi.org\/10.1145\/1709093.1709095","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2010,3]]},"assertion":[{"value":"2007-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-07-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-03-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}