We present an automated approach to prove termination of Java Bytecode (JBC) programs
by automatically transforming them to term rewrite systems
(TRSs). In this way, the numerous techniques and tools developed for
TRS termination can now also be used for imperative object-oriented
languages like Java, which can be compiled into JBC.
A full version of our paper including all proofs is available here.
Implementation in AProVE
A new version of the
termination tool AProVE implementing our approach is available here. In particular, this
new version of AProVE allows to repeat the experiments
below. It can be accessed via a web
interface.
The web interface takes an arbitrary jar-file as input. As in the
International Termination Competition, it then tries to prove termination of the main method of the class that is indicated in the file META-INF/MANIFEST.MF. For details, please see the definition of JBC termination problems. In order to prove termination of a specific method, one therefore has to add an appropriate main method calling the specific method with random inputs.
Tools
We compare our implementation with two other tools for termination analysis of Java Bytecode. Thus, in our experiments we use the following three tools:
- AProVE
This is a new version of AProVE which is available through our web interface.
For AProVE, we ran the experiments using an Intel Core i7 920 CPU with four CPU cores and 2.66 GHz each.
- Julia
Julia is a nullness and termination analyzer for Java Bytecode based on path-length abstraction, developed at the University of Verona, Italy and the University of Réunion, France.
The Julia team kindly provided us with access to a web interface running the current version of Julia.
We performed the experiments on 21st of January, 2010. The Julia web interface was powered by an Intel Xeon CPU with four CPU cores and 2.66GHz each.
- COSTA
COSTA is a cost and termination analyzer for Java Bytecode based on path-length abstraction, developed at the Politécnica University of Madrid and the Complutense University of Madrid, Spain.
The results for the experiments with COSTA were kindly provided by the COSTA team. The computer used for these experiments was an Intel Core 2 CPU with two CPU cores and 1.86 GHz each.
Examples
In our experiments, we tested the tools on the 106 non-recursive JBC examples from the termination problem data base (TPDB) used in the International Termination Competition.
We removed one controversial example ("overflow") from the TPDB whose termination depends on the treatment of integer overflows. Furthermore, we added the two examples "count" and "flatten" from our paper.
In the experiments, we used a timeout of 60 seconds for each example. This is the same timeout that is used in the International Termination Competition.
The tables below summarize our experiments. They show that for the problems in the current example collection,
our rewriting-based approach in AProVE currently yields the most
precise results.
The main reason is that we do not use a fixed abstraction from data objects to integers, but represent objects as terms.
On the other hand, this also explains the longer runtimes of AProVE compared to Julia and COSTA. Still, our approach is efficient enough to solve most examples in reasonable time.
Our method benefits substantially from the representation of objects as terms, since afterwards arbitrary TRS termination techniques can be used to prove termination of the algorithms. Of course,
while the examples in the TPDB are challenging, they are still quite small.
Future work will be concerned with the application and adaption of our
approach in order to use it also for large examples and Java
libraries. Moreover,
in the current paper, we restricted ourselves to JBC programs without recursion. Of course, an extension of our method to recursive programs is another main point for future work.
In the following table
Success gives the number of examples where termination
was proved, Failure means that the proof failed in less than 60 seconds,
Timeout gives the number of examples where the tool took longer than 60 seconds, and
Runtime is the average time needed per example.
| Tool | Success | Failure | Timeout | Runtime |
|---|
| AProVE | 89 | 5 | 12 | 14.3 sec |
| Julia | 74 | 32 | 0 | 2.6 sec |
| Costa | 60 | 46 | 0 | 3.4 sec |
In the following table, each row shows the behavior of the tools on one
example. The entry "YES" means that termination of that example could be proved
by the corresponding tool while "MAYBE" states that the tool gave up without
success. Finally, "TIMEOUT" indicates that the tool exceeded the given time
limit and was therefore stopped. By clicking on the respective runtime, one can
inspect the output produced by the tool. (For COSTA, we did not receive the proofs.)
To load an example into the web interface of AProVE, just click on the corresponding
button in the first column. Then you can run AProVE on the respective example
yourself.
Of those examples, 10 are known to be non-terminating, which can be
easily proved manually. The corresponding lines contain the remark "(non-term.)".
When using the AProVE web interface, please keep in mind that the computer running the web interface is considerably slower (four AMD Opteron CPU cores with 2.2GHz each) than the one used for the experiments. Therefore,
a higher timeout of up to 300 seconds is needed to solve all examples that AProVE could solve in the table below.
Please also keep in mind that the computer used for the web interface is used by several other applications as well, so the runtimes may vary.