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 <>
Submitted on : Thursday, November 15, 2018 - 12:26:22 PM
Last modification on : Monday, September 2, 2019 - 9:41:33 AM


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⟩