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 metadatas

http://hal.univ-reunion.fr/hal-01188696
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

File

Experiments_with_non_terminati...
Explicit agreement for this submission

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

62

Files downloads

109