Non-termination of Dalvik bytecode via compilation to CLP

TL;DR

This paper introduces a compilation method transforming Dalvik bytecode into logic programs with array constraints, enabling the use of existing non-termination analysis techniques to determine if Dalvik programs do not terminate.

Contribution

It presents a novel compilation approach from Dalvik bytecode to constraint logic programs, facilitating non-termination proofs for Dalvik programs using existing methods.

Findings

Compilation rules effectively translate Dalvik bytecode into logic programs

Non-termination of the compiled program implies non-termination of the original

Enables application of existing non-termination analysis techniques to Dalvik programs

Abstract

We present a set of rules for compiling a Dalvik bytecode program into a logic program with array constraints. Non-termination of the resulting program entails that of the original one, hence the techniques we have presented before for proving non-termination of constraint logic programs can be used for proving non-termination of Dalvik programs.