In earlier work,
we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to prove termination of JBC automatically. In this paper, we improve this approach substantially in two ways:
We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.
- We extend it in order to also analyze recursive JBC programs. To this end, one has to represent call stacks of arbitrary size.
- To handle JBC programs with several methods, we modularize our approach in order to re-use termination graphs and TRSs for the separate methods and to prove termination of the resulting TRS in a modular way.
Here, we provide links to our papers. The extended versions of the respective papers include all proofs.
- M. Brockschmidt, C. Otto, and J. Giesl
Modular Termination Proofs of Recursive Java Programs by Term Rewriting
Submitted to RTA 2011.
Extended version including all proofs
appeared as Technical Report AIB-2011-02, RWTH Aachen, Germany.
- M. Brockschmidt, C. Otto, C. von Essen, and J. Giesl
Termination Graphs for Java Bytecode
In Verification, Induction, Termination Analysis, LNAI 6463, pages 17-37, 2010.
Extended version including all proofs appeared as Technical Report AIB-2010-15, RWTH Aachen, Germany.
- C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
Automated Termination Analysis of Java Bytecode by Term Rewriting
In Proceedings of the 21th International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010.
Extended version including all proofs
appeared as Technical Report AIB-2010-08, RWTH Aachen, Germany.
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
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.
We compare our implementation with the previous version of AProVE and with
two other tools for termination analysis of Java Bytecode. Thus, in our experiments we use the following four tools:
- AProVE 2011
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 950 CPU with four CPU cores and 3.06 GHz each.
- AProVE 2010
This is the previous version of AProVE
which implements the technique of our papers from 2010. The main difference to AProVE 2011 is that
it does not perform modular proofs and that it cannot deal with recursion (except in special cases, where one just has to evaluate methods with fixed inputs). For more details on AProVE 2010 and to run this previous version of AProVE via a web interface, we refer to the
evaluation web site of our RTA 2010 paper.
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, 2011. The Julia web interface was powered by an Intel Xeon CPU with four CPU cores and 2.66GHz each.
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 i5 650 CPU with 2 CPU cores and 3.2 GHz each.
In our experiments, we tested the tools on 83 recursive and 133 non-recursive JBC examples. These
examples contain the 172 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.
In the experiments, we used a timeout of 120 seconds for each example.
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. (However, there are also several examples
where Julia or COSTA succeed whereas AProVE fails.)
The main reason for the power of AProVE
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.
In the following table,
Yes gives the number of examples where termination
was proved, Maybe means that the proof failed in less than 120 seconds,
Timeout gives the number of examples where the tool took longer than 120 seconds, and
Runtime is the average time in seconds needed per example.
Recursive examples (83)
|AProVE 2011||67||0||16||30 sec|
|AProVE 2010||15||3||65||96 sec|
Non-Recursive examples (133)
|AProVE 2011||108||0||25||27 sec|
|AProVE 2010||103||13||17||23 sec|
In the following tables, 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
Of those examples, 15 are known to be non-terminating, which can
easily be 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 600 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.