Experiments with Non-Termination Analysis for Java Bytecode - Université de La Réunion Access content directly
Conference Papers Year : 2009

Experiments with Non-Termination Analysis for Java Bytecode


Non-termination analysis proves that programs, or parts of a program, do not terminate. This is important since non-termination is often an unexpected behaviour of computer programs and exposes a bug in their code. While research has found ways of proving non-termination of logic programs and of term rewriting systems, this is hardly the case for imperative programs. In this paper, we describe and experiment with a technique for proving non-termination of imperative, bytecode programs by relating their non-termination to that of a (constraint) logic program. Moreover, we show that our non-termination test effectively helps a termination test, by avoiding expensive search for termination proofs of those portions of the code where such proofs do not exist.
Fichier principal
Vignette du fichier
Experiments_with_non_termination_analysis_for_java_bytecode_hal.pdf (3.37 Mo) Télécharger le fichier
Origin Explicit agreement for this submission

Dates and versions

hal-01188696 , version 1 (07-06-2018)
hal-01188696 , version 2 (15-11-2018)



Etienne Payet, Fausto Spoto. Experiments with Non-Termination Analysis for Java Bytecode. Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), Mar 2009, York, United Kingdom. pp.83--96, ⟨10.1016/j.entcs.2009.11.016⟩. ⟨hal-01188696v2⟩
87 View
225 Download



Gmail Mastodon Facebook X LinkedIn More