HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Experiments with Non-Termination Analysis for Java Bytecode

Résumé : 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.
Document type :
Conference papers
Complete list of metadata

Contributor : Réunion Univ Connect in order to contact the contributor
Submitted on : Thursday, November 15, 2018 - 12:26:22 PM
Last modification on : Monday, March 21, 2022 - 5:22:04 PM


Explicit agreement for this submission




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⟩



Record views


Files downloads