Non-termination analysis proves that programs, or parts of a program, do notterminate. This is important since non-termination is often an unexpectedbehaviour of computer programs and exposes a bug in their code.While research has found ways of proving non-termination of logic programsand of term rewriting systems, this is hardly the case for imperative programs.In this paper, we describe and experiment with a technique for provingnon-termination of imperative, bytecode programs by relating theirnon-termination to that of a (constraint) logic program. Moreover, we showthat our non-termination test effectively helps a termination test,by avoiding expensive search for termination proofs of thoseportions of the code where such proofs do not exist.

Experiments with Non-Termination Analysis for Java Bytecode

SPOTO, Nicola Fausto
2009

Abstract

Non-termination analysis proves that programs, or parts of a program, do notterminate. This is important since non-termination is often an unexpectedbehaviour of computer programs and exposes a bug in their code.While research has found ways of proving non-termination of logic programsand of term rewriting systems, this is hardly the case for imperative programs.In this paper, we describe and experiment with a technique for provingnon-termination of imperative, bytecode programs by relating theirnon-termination to that of a (constraint) logic program. Moreover, we showthat our non-termination test effectively helps a termination test,by avoiding expensive search for termination proofs of thoseportions of the code where such proofs do not exist.
Static analysis; abstract Interpretation; non-termination analysis; termination analysis; Java bytecode
File in questo prodotto:
File Dimensione Formato  
ExperimentsNonTermination.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 287.94 kB
Formato Adobe PDF
287.94 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/339419
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact