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.
Type de document :
Communication dans un congrès
Elvira Albert. Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), Mar 2009, York, United Kingdom. Elsevier, 253-5 (5), pp.83--96, 2009, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2009.11.016〉
Liste complète des métadonnées

http://hal.univ-reunion.fr/hal-01188696
Contributeur : Réunion Univ <>
Soumis le : jeudi 15 novembre 2018 - 12:26:22
Dernière modification le : vendredi 16 novembre 2018 - 01:40:58

Fichier

Experiments_with_non_terminati...
Accord explicite pour ce dépôt

Identifiants

Collections

Citation

Etienne Payet, Fausto Spoto. Experiments with Non-Termination Analysis for Java Bytecode. Elvira Albert. Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), Mar 2009, York, United Kingdom. Elsevier, 253-5 (5), pp.83--96, 2009, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2009.11.016〉. 〈hal-01188696v2〉

Partager

Métriques

Consultations de la notice

9

Téléchargements de fichiers

4