Experimental Evaluation of "Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting"

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 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.

We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.

Literature

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 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 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
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
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.

Examples

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)

Tool	Yes	Maybe	Timeout	Runtime
AProVE 2011	67	0	16	30 sec
AProVE 2010	15	3	65	96 sec
Julia	57	26	0	3 sec
COSTA	47	35	1	6 sec

Non-Recursive examples (133)

Tool	Yes	Maybe	Timeout	Runtime
AProVE 2011	108	0	25	27 sec
AProVE 2010	103	13	17	23 sec
Julia	96	37	0	2 sec
COSTA	73	60	0	5 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 yourself. 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.

Recursive examples

Example	AProVE 2011		AProVE 2010		Julia		COSTA
	YES	7.12	TIMEOUT	120	YES	4.39	YES	3.08
	YES	12.91	YES	13.25	YES	1.9	YES	0.69
	YES	9.9	TIMEOUT	120	YES	1.73	YES	0.55
	YES	2.78	TIMEOUT	120	YES	2.15	MAYBE	1.21
	YES	2.15	TIMEOUT	120	YES	1.64	MAYBE	1.18
	YES	6.15	TIMEOUT	120	MAYBE	4.95	MAYBE	4.35
	YES	1.65	MAYBE	48.84	MAYBE	1.88	MAYBE	2.15
	YES	4.94	TIMEOUT	120	MAYBE	2.75	YES	0.67
	YES	9.12	TIMEOUT	120	MAYBE	4.12	YES	4.1
	YES	5.25	TIMEOUT	120	MAYBE	3.59	YES	2.44
	YES	28.11	TIMEOUT	120	YES	3.0	MAYBE	3.92
	YES	66.4	TIMEOUT	120	MAYBE	2.94	MAYBE	8.35
	YES	5.25	TIMEOUT	120	MAYBE	2.5	MAYBE	4.37
	YES	5.44	TIMEOUT	120	MAYBE	2.4	MAYBE	12.25
	YES	7.93	TIMEOUT	120	MAYBE	2.4	MAYBE	7.27
	YES	6.13	TIMEOUT	120	MAYBE	2.55	MAYBE	4.83
	YES	5.48	TIMEOUT	120	MAYBE	2.5	MAYBE	4.84
	TIMEOUT	120	TIMEOUT	120	MAYBE	2.54	MAYBE	31.51
	YES	5.93	TIMEOUT	120	MAYBE	2.65	YES	2.74
	YES	1.7	TIMEOUT	120	YES	1.5	YES	0.21
	YES	1.99	TIMEOUT	120	YES	1.49	YES	0.08
	YES	7.39	TIMEOUT	120	MAYBE	4.16	YES	7.06
	YES	7.31	TIMEOUT	120	MAYBE	5.16	YES	5.3
	YES	5.48	TIMEOUT	120	MAYBE	2.8	MAYBE	4.2
	YES	4.89	TIMEOUT	120	MAYBE	2.84	YES	2.54
	YES	13.9	TIMEOUT	120	MAYBE	2.17	YES	0.6
	YES	13.33	TIMEOUT	120	YES	2.15	MAYBE	1.69
	YES	8.44	TIMEOUT	120	MAYBE	2.89	MAYBE	11.17
	YES	1.57	TIMEOUT	120	YES	1.49	YES	0.2
	YES	2.11	TIMEOUT	120	YES	1.59	MAYBE	0.84
	YES	5.69	TIMEOUT	120	MAYBE	2.47	MAYBE	8.63
	YES	18.32	TIMEOUT	120	MAYBE	2.7	MAYBE	12.96
	YES	1.58	TIMEOUT	120	YES	1.45	MAYBE	0.46
	YES	14.45	TIMEOUT	120	MAYBE	4.95	YES	18.41
	YES	10.48	MAYBE	50.46	YES	3.11	YES	4.4
	YES	9.32	TIMEOUT	120	YES	2.61	TIMEOUT	120.0
	YES	4.94	TIMEOUT	120	YES	2.17	YES	0.6
	YES	4.84	TIMEOUT	120	YES	2.25	MAYBE	3.49
	YES	2.32	TIMEOUT	120	YES	1.48	YES	1.18
	YES	1.29	TIMEOUT	120	YES	1.44	YES	0.05
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.39	MAYBE	0.26
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.47	MAYBE	0.21
	YES	2.72	TIMEOUT	120	YES	1.65	YES	0.38
	YES	1.47	TIMEOUT	120	YES	1.67	YES	0.19
	YES	2.81	TIMEOUT	120	YES	1.74	YES	1.24
	YES	1.2	YES	1.23	YES	2.0	YES	0.86
	YES	1.51	YES	1.55	YES	1.84	YES	0.43
	TIMEOUT	120	TIMEOUT	120	YES	14.8	MAYBE	0.0
	YES	1.53	YES	7.9	YES	1.44	YES	0.06
	YES	1.33	YES	3.24	YES	1.39	YES	0.05
	YES	1.81	YES	8.16	YES	1.44	YES	0.08
	YES	1.05	YES	1.3	YES	1.59	YES	0.03
	YES	1.4	YES	1.24	YES	1.69	YES	0.06
	YES	1.03	YES	1.12	YES	1.94	YES	0.17
	YES	1.21	YES	1.19	YES	1.79	YES	0.25
	YES	1.17	YES	1.2	YES	4.15	YES	1.89
	YES	1.17	YES	1.19	YES	4.0	YES	2.06
	TIMEOUT	120	TIMEOUT	120	YES	2.81	MAYBE	0.0
	TIMEOUT	120	TIMEOUT	120	YES	6.09	YES	9.45
	TIMEOUT	120	TIMEOUT	120	YES	2.35	MAYBE	0.0
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.39	MAYBE	0.15
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.74	MAYBE	0.72
	YES	1.63	YES	1.66	YES	1.83	MAYBE	1.1
	YES	3.0	TIMEOUT	120	YES	1.64	YES	1.47
	YES	3.15	TIMEOUT	120	YES	2.04	YES	0.62
	YES	7.4	YES	6.81	YES	2.2	YES	1.13
	YES	2.93	TIMEOUT	120	YES	1.99	YES	0.42
	YES	3.18	TIMEOUT	120	YES	2.05	YES	0.42
	YES	1.93	TIMEOUT	120	YES	1.88	YES	0.41
	TIMEOUT	120	TIMEOUT	120	YES	17.24	MAYBE	77.62
	TIMEOUT	120	TIMEOUT	120	YES	3.7	YES	2.44
	TIMEOUT	120	MAYBE	48.31	YES	5.49	MAYBE	47.66
	YES	17.92	TIMEOUT	120	YES	2.29	YES	1.14
	TIMEOUT	120	TIMEOUT	120	YES	2.94	YES	0.33
	YES	44.02	TIMEOUT	120	YES	7.54	MAYBE	0.0
	YES	3.05	YES	8.88	YES	1.55	MAYBE	0.4
	YES	5.38	TIMEOUT	120	YES	1.93	YES	0.35
	YES	2.82	TIMEOUT	120	YES	11.25	YES	0.21
	YES	88.09	TIMEOUT	120	YES	3.59	YES	11.48
	TIMEOUT	120	TIMEOUT	120	YES	3.59	MAYBE	0.0
	YES	22.88	TIMEOUT	120	YES	2.49	MAYBE	5.0
	TIMEOUT	120	TIMEOUT	120	YES	37.05	MAYBE	0.0
	TIMEOUT	120	TIMEOUT	120	YES	8.45	YES	8.81

Non-Recursive examples

Example	AProVE 2011		AProVE 2010		Julia		COSTA
	YES	2.71	YES	3.59	YES	1.89	YES	0.31
	TIMEOUT	120	TIMEOUT	120	MAYBE	1.64	MAYBE	0.76
	YES	4.68	YES	4.98	YES	2.25	MAYBE	2.54
	YES	9.26	YES	22.26	MAYBE	4.9	MAYBE	49.38
	YES	6.02	YES	15.52	MAYBE	3.19	MAYBE	30.28
	YES	2.32	YES	1.73	YES	1.7	YES	0.25
	YES	3.51	YES	2.98	YES	1.64	YES	0.34
	YES	2.09	YES	1.78	YES	1.54	YES	0.23
	YES	18.07	YES	2.66	YES	1.79	YES	1.76
	YES	2.01	YES	2.1	YES	1.59	YES	0.22
	YES	6.82	YES	8.51	YES	3.64	MAYBE	22.35
	YES	7.28	YES	7.31	MAYBE	3.9	MAYBE	43.65
	YES	6.03	YES	6.31	MAYBE	4.65	MAYBE	48.66
	YES	24.21	YES	4.06	MAYBE	1.69	MAYBE	0.98
	YES	15.81	YES	2.58	MAYBE	1.55	MAYBE	1.0
	YES	15.77	YES	3.04	MAYBE	1.59	MAYBE	0.97
	YES	22.37	YES	11.85	YES	1.54	MAYBE	0.84
	YES	35.34	TIMEOUT	120	MAYBE	1.59	MAYBE	1.33
	YES	5.92	YES	10.14	MAYBE	2.59	MAYBE	16.61
	YES	4.06	YES	2.38	YES	2.1	YES	0.55
	YES	3.68	YES	2.18	YES	1.89	YES	0.61
	YES	12.36	YES	8.18	YES	2.14	YES	0.7
	YES	2.83	YES	11.89	YES	2.49	MAYBE	6.37
	YES	11.81	YES	7.35	MAYBE	1.59	MAYBE	0.72
	YES	1.59	YES	1.71	YES	1.54	YES	0.19
	YES	2.45	YES	2.23	YES	1.55	MAYBE	0.83
	YES	11.41	YES	6.7	MAYBE	1.64	MAYBE	0.76
	YES	1.81	TIMEOUT	120	YES	1.6	MAYBE	0.69
	TIMEOUT	120	TIMEOUT	120	MAYBE	1.53	MAYBE	1.16
	YES	1.55	YES	1.7	YES	1.59	YES	0.2
	YES	1.87	MAYBE	2.93	YES	1.55	MAYBE	0.76
	TIMEOUT	120	TIMEOUT	120	MAYBE	1.51	MAYBE	0.84
	YES	5.96	YES	8.98	MAYBE	3.5	MAYBE	18.89
	YES	74.21	YES	2.34	YES	1.56	YES	0.29
	YES	5.42	YES	4.96	YES	1.54	YES	0.29
	YES	1.57	YES	1.87	YES	1.54	YES	0.23
	YES	1.51	YES	1.75	YES	1.56	YES	0.15
	YES	1.52	YES	1.77	YES	1.52	YES	0.13
	YES	1.74	YES	1.75	YES	1.49	YES	0.19
	YES	1.8	YES	1.85	YES	1.54	YES	0.23
	YES	1.53	YES	1.78	YES	1.44	YES	0.19
	YES	1.99	YES	2.06	YES	1.45	YES	0.2
	YES	1.99	YES	1.97	YES	1.49	YES	0.23
	YES	1.92	YES	2.03	YES	1.6	YES	0.29
	YES	1.68	YES	1.55	YES	1.56	YES	0.41
	YES	5.19	YES	7.97	YES	1.64	YES	0.93
	YES	1.58	YES	2.23	YES	1.46	YES	0.24
	YES	1.76	YES	2.7	YES	1.54	YES	0.28
	YES	1.68	YES	2.11	YES	1.5	YES	0.21
	YES	2.14	YES	2.36	YES	1.55	YES	0.22
	YES	2.93	YES	3.37	YES	1.54	YES	0.25
	YES	1.59	YES	1.78	YES	1.44	YES	0.17
	YES	1.59	YES	1.68	YES	1.44	YES	0.19
	YES	1.78	YES	1.7	YES	1.44	YES	0.18
	YES	1.61	YES	1.88	YES	1.44	YES	0.21
	YES	1.35	YES	1.49	YES	1.44	YES	0.2
	YES	1.59	YES	1.5	YES	1.46	YES	0.22
	YES	1.84	YES	1.8	YES	1.5	YES	0.24
	YES	2.07	YES	3.36	YES	1.48	YES	0.24
	YES	30.51	YES	4.74	YES	1.64	YES	0.26
	YES	3.39	YES	10.92	YES	1.48	YES	0.37
	YES	2.26	YES	2.54	YES	1.64	YES	0.2
	YES	2.61	YES	1.99	YES	1.58	YES	0.2
	YES	3.23	YES	2.07	YES	1.54	YES	1.92
	TIMEOUT	120	TIMEOUT	120	MAYBE	1.6	YES	0.26
	YES	1.96	YES	1.68	YES	1.54	YES	0.26
	YES	5.7	YES	3.76	YES	1.69	YES	0.35
	YES	2.03	YES	2.09	YES	1.54	MAYBE	0.96
	TIMEOUT	120	YES	12.07	MAYBE	1.41	MAYBE	0.56
	YES	2.23	YES	1.85	YES	1.99	YES	2.0
	TIMEOUT	120	YES	12.94	MAYBE	5.4	MAYBE	15.37
	YES	4.54	YES	3.04	YES	2.54	MAYBE	2.94
	TIMEOUT	120	TIMEOUT	120	YES	2.68	MAYBE	5.62
	YES	1.83	YES	1.55	YES	1.5	YES	0.07
	YES	2.78	YES	1.95	YES	1.8	YES	0.81
	YES	2.16	YES	2.26	YES	1.55	YES	0.19
	YES	1.07	YES	1.21	MAYBE	1.43	MAYBE	0.99
	YES	3.69	YES	3.05	YES	1.79	YES	0.51
	YES	1.09	YES	1.14	MAYBE	1.69	MAYBE	1.3
	YES	1.07	YES	1.15	MAYBE	1.61	MAYBE	2.42
	TIMEOUT	120	YES	6.88	YES	3.3	MAYBE	18.8
	YES	7.95	YES	12.64	MAYBE	4.44	MAYBE	59.93
	YES	1.05	YES	1.31	YES	1.43	MAYBE	0.95
	YES	1.05	YES	1.21	MAYBE	1.39	MAYBE	0.55
	YES	1.7	YES	1.69	MAYBE	1.54	YES	0.38
	YES	5.94	YES	8.01	YES	2.54	YES	1.03
	YES	1.06	YES	1.13	YES	1.59	MAYBE	1.54
	YES	1.14	YES	1.4	MAYBE	1.99	MAYBE	10.9
	YES	1.05	YES	1.32	MAYBE	1.65	MAYBE	0.91
	YES	1.01	YES	1.48	YES	1.35	YES	0.03
	YES	10.86	MAYBE	47.34	YES	1.83	YES	0.66
	YES	1.06	YES	1.12	YES	1.4	YES	0.04
(non-term.)	TIMEOUT	120	MAYBE	46.89	MAYBE	1.4	MAYBE	0.16
	YES	2.68	YES	1.8	YES	1.88	MAYBE	0.17
	YES	1.72	YES	1.59	YES	1.64	MAYBE	0.1
	YES	1.05	YES	1.41	YES	1.36	MAYBE	0.07
	YES	1.18	YES	1.21	YES	1.79	MAYBE	0.12
(non-term.)	TIMEOUT	120	MAYBE	47.4	MAYBE	1.39	MAYBE	0.12
(non-term.)	TIMEOUT	120	MAYBE	49.54	MAYBE	2.28	MAYBE	5.66
	YES	1.32	YES	1.37	YES	3.54	YES	1.53
(non-term.)	TIMEOUT	120	MAYBE	48.46	MAYBE	1.51	MAYBE	0.47
(non-term.)	TIMEOUT	120	MAYBE	47.9	MAYBE	1.44	MAYBE	0.21
	YES	1.17	YES	1.16	YES	1.44	YES	0.07
(non-term.)	TIMEOUT	120	MAYBE	48.2	MAYBE	1.39	MAYBE	0.22
	YES	1.15	YES	1.2	YES	1.41	YES	0.07
	YES	1.07	YES	1.29	YES	1.5	YES	0.1
(non-term.)	TIMEOUT	120	MAYBE	46.77	MAYBE	1.36	MAYBE	0.57
	TIMEOUT	120	TIMEOUT	120	YES	3.71	YES	11.07
	YES	4.73	MAYBE	13.68	YES	3.09	MAYBE	8.02
	YES	1.41	YES	1.46	YES	1.4	YES	0.06
	YES	1.29	YES	1.25	YES	1.49	YES	0.06
	YES	1.28	YES	1.34	YES	1.4	YES	0.06
	YES	1.07	YES	1.13	YES	1.99	YES	0.45
(non-term.)	TIMEOUT	120	MAYBE	47.65	MAYBE	1.43	MAYBE	0.78
(non-term.)	TIMEOUT	120	MAYBE	46.64	MAYBE	1.55	MAYBE	0.01
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.94	MAYBE	0.8
	YES	1.05	YES	1.17	YES	1.49	MAYBE	0.35
	YES	1.12	YES	1.15	YES	2.92	YES	3.47
	YES	4.17	YES	6.32	YES	2.64	YES	1.36
	TIMEOUT	120	TIMEOUT	120	YES	12.64	MAYBE	77.73
	TIMEOUT	120	MAYBE	35.42	YES	14.04	MAYBE	0.0
	YES	25.8	YES	31.76	YES	6.6	YES	10.84
	TIMEOUT	120	TIMEOUT	120	YES	5.15	YES	0.44
	YES	1.05	YES	1.14	YES	1.54	MAYBE	1.12
	TIMEOUT	120	TIMEOUT	120	YES	18.3	MAYBE	88.94
	YES	4.47	TIMEOUT	120	YES	2.0	YES	0.35
(non-term.)	TIMEOUT	120	TIMEOUT	120	MAYBE	1.9	MAYBE	2.0
	YES	3.66	YES	2.92	YES	2.04	YES	0.29
	YES	10.26	TIMEOUT	120	YES	3.84	YES	8.29
	YES	13.94	TIMEOUT	120	YES	4.29	YES	40.68
	YES	5.86	YES	25.31	YES	2.8	MAYBE	5.35
	YES	4.56	YES	10.8	YES	2.33	MAYBE	1.13
	TIMEOUT	120	TIMEOUT	120	YES	2.99	YES	6.32