https://hal.univ-reunion.fr/hal-01916989Spoto, FaustoFaustoSpotoUNIVR | DI - Department of Computer Science [Verona] - UNIVR - Università degli studi di Verona = University of VeronaMesnard, FrédéricFrédéricMesnardIREMIA - Institut de REcherche en Mathématiques et Informatique Appliquées - UR - Université de La RéunionPayet, EtienneEtiennePayetIREMIA - Institut de REcherche en Mathématiques et Informatique Appliquées - UR - Université de La RéunionA Termination Analyser for Java Bytecode Based on Path-LengthHAL CCSD2010Javatermination analysisTheoryVerification Additional Key Words and Phrases: Abstract interpretationJava bytecodeSpecifying and Verifying and Reasoning about Programs-Mechanical VerificationSemantics of Programming Languages-Denotational SemanticsProgram Analysis General Terms: Languages[INFO] Computer Science [cs][INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]Univ, Réunion2018-11-09 07:18:472022-03-21 17:22:042018-11-23 07:18:01enJournal articlesapplication/pdf1It 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, non-trivial subset of the terminating programs. In this paper we present our termination analyser for sequential Java bytecode, based on a program property called path-length. 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 w.r.t. a reference denotational semantics of the bytecode. We show that a constraint logic program P CLP can be built from the result of the path-length analysis of a Java bytecode program P and formally prove that if P CLP terminates then also P terminates. Hence a termination prover for constraint logic programs can be applied to prove the termination of P. We conclude with some discussion of the possibilities and limitations of our approach. Ours is the first existing termination analyser 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.