Recently, we developed an approach for automated termination proofs of Java Bytecode
(JBC), which is based on constructing and analyzing termination graphs. These
graphs represent all possible program executions in a finite way. In this paper, we show
that this approach can also be used to detect non-termination or NullPointerExceptions.
Our approach automatically
generates witnesses, i.e., calling the JBC method
with these witness arguments indeed leads to non-termination resp. to
a NullPointerException. Thus, we never obtain "false positives".
We implemented our results in the termination prover AProVE and provide experimental
evidence for the power of our approach.
Here, we provide links to our papers on analyzing Java Bytecode. The extended versions of the respective papers include all proofs.
- M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
In Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in Computer Science. To appear.
Extended version appeared as Technical Report AIB-2011-19, RWTH Aachen, Germany.
- M. Brockschmidt, C. Otto, and J. Giesl
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia,
LIPIcs Leibniz International Proceedings in Informatics 10, pages 155-170, 2011.
Extended version 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 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 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 (non-)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 (non-)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
two other tools for (non-)termination analysis of Java. Thus, in our experiments we use the following four tools:
- AProVE 2011-No
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 2011
This is the old version of AProVE which implements only the techniques from earlier papers.
The main difference to AProVE 2011-No is that it is not able to prove non-termination. For more details on AProVE 2011 and to run this previous version of AProVE via a web interface, we refer to the
evaluation web site of our RTA 2011 paper.
Julia is a nullness and (non-)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 July 26, 2011. The Julia web interface was powered by an Intel Xeon CPU with four CPU cores and 2.66GHz each.
Invel is a tool for detecting non-termination of Java programs. It is based on the KeY system which is developed at the Karlsruhe Institute of Technology, Germany and the Chalmers University of Technology of Gothenburg, Sweden.
As we were not able to obtain a running version of Invel, we have used the results reported in the detailed description of the tool. However, this description does not provide runtimes.
In our experiments, we tested the tools on a collection of 325 examples.
These examples have been taken from three sources:
In the experiments, we used a timeout of 60 seconds for each example.
- the 2 examples from our paper.
- the 268 Java Bytecode examples from the Termination Problem Data Base (TPDB), which is used in the International Termination Competition.
However, we removed one controversial example ("Overflow") from the TPDB whose termination depends on the treatment of integer overflows.
- the 55 examples from the evaluation of Invel.
The tables below summarize our experiments. They show that for the problems in the current example collection,
AProVE currently yields the most precise results both for termination and non-termination analysis.
(However, there are also several examples where Julia could prove termination whereas AProVE fails.)
In the following table,
Yes gives the number of examples where termination was proven,
No gives the number of examples where non-termination was proven,
Maybe 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 in seconds needed per example.
TPDB and our examples (270)
|AProVE 2011-No||204||30|| 12|| 24|| 11.2|
|AProVE 2011 ||204|| 0|| 27|| 39|| 14.5|
|Julia ||166||22|| 82|| 0|| 3.9|
Invel examples (55)
|AProVE 2011-No|| 1||51|| 0|| 3|| 5.1|
|AProVE 2011 || 1|| 0|| 5|| 49|| 54.0|
|Julia || 1|| 0|| 54|| 0|| 2.2|
|Invel || 0||42|| 13|| 0|| ?|
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,
"NO" means that non-termination could be proved,
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, but note that for Invel, we have no 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, 90 are known to be non-terminating. The corresponding lines contain the remark "(non-term.)". Moreover, 233 examples
are known to be terminating, and for 2 examples, the termination behavior is unknown (they are variations of the Collatz function).
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.
TPDB and our examples