It is important to prove that supposedly terminating programs actuallyterminate, particularly if those programs must berun 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 provetermination 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 theanalyses which are needed before the path-length can be computed, such assharing, cyclicity and aliasing. Then weformally define the path-length analysis and prove it correct wrt areference denotational semantics of the bytecode. We show that a constraintlogic program P_CLPcan be built from the result of the path-length analysisof a Java bytecode program P andformally prove that if P_CLP terminates then also P terminates.Hence a termination prover for constraint logic programs can be appliedto prove the termination of P. We conclude with some discussion of thepossibilities and limitations of our approach.Ours is the first existing termination analyser for Java bytecodedealing with any kind of data structures dynamically allocated on the heapand which does not require any help or annotation on the part of the user.

A Termination Analyzer for Java Bytecode based on Path-Length

SPOTO, Nicola Fausto;
2010

Abstract

It is important to prove that supposedly terminating programs actuallyterminate, particularly if those programs must berun 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 provetermination 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 theanalyses which are needed before the path-length can be computed, such assharing, cyclicity and aliasing. Then weformally define the path-length analysis and prove it correct wrt areference denotational semantics of the bytecode. We show that a constraintlogic program P_CLPcan be built from the result of the path-length analysisof a Java bytecode program P andformally prove that if P_CLP terminates then also P terminates.Hence a termination prover for constraint logic programs can be appliedto prove the termination of P. We conclude with some discussion of thepossibilities and limitations of our approach.Ours is the first existing termination analyser for Java bytecodedealing with any kind of data structures dynamically allocated on the heapand which does not require any help or annotation on the part of the user.
static analysis; abstract interpretation; termination analysis; Java bytecode; path-length
File in questo prodotto:
File Dimensione Formato  
toplas2010.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Dominio pubblico
Dimensione 1.19 MB
Formato Adobe PDF
1.19 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/332031
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 89
  • ???jsp.display-item.citation.isi??? 59
social impact