Non-Termination Analysis of Java Bytecode

TL;DR

This paper presents a fully automated static analysis method for Java bytecode that can prove the existence of infinite executions, including infinite recursion, which was not possible with previous tools.

Contribution

It introduces a novel approach that compiles Java bytecode into constraint logic programs and proves non-termination, handling method calls and infinite recursion.

Findings

Julia detected non-termination in cases where other tools failed.

The approach successfully proved non-termination for a set of 113 programs.

It is the first static method capable of proving infinite recursion in Java bytecode.

Abstract

We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The technique consists in compiling P into a constraint logic program P_CLP and in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implemented our technique inside the Julia analyser. We have compared the results of Julia on a set of 113 programs with those provided by AProVE and Invel, the only freely usable non-termination analysers comparable to ours that we are aware of. Only Julia could detect non-termination due to infinite recursion.