Experimental Evaluation of "Better termination proving through cooperation"

Implementation

Details on the implementation, and the sources of the tool, can be found on the T2 website.

Tools

We compare the following tools:

Terminator, which implements an oscillation between rank function synthesis and safety using termination arguments expressed as transition invariants.
T2, which implements a Terminator-like oscillation between rank function synthesis and safety using termination arguments expressed as lexicographic rank functions.
Cooperating-T2, our T2-based implementation of "Better termination proving through cooperation"
ARMC, which also implements a Terminator-like procedure.
AProVE, a termination prover based on the dependency pair framework. AProVE does not generate invariants on demand and hence always uses the supporting invariant true.
AProVE+Interproc, which uses the abstract interpretation tool Interproc to generate as many invariants as possible using the Octagon abstract domain before running AProVE.
Size-Change/MCNP, an implementation of termination proofs via monotonicity constraints, an efficient generalization of the size change principle. The abstraction from integer programs to monotonicity constraints is implemented in AProVE.
KITTeL, another termination prover based on termination proving techniques from rewriting systems.

Examples

During our evaluation we ran tools on a set of 449 termination proving benchmarks drawn from a variety of application (e.g. Windows device drivers, the Apache web server, the PostgreSQL server, integer approximations of numerical programs from a book on numerical recipes, integer approximations of benchmarks from LLBMC and other tool evaluations). The examples are available in T2s internal integer transition system format and in an equivalent translation to C. Note that these C examples are obtained from an automatic translation from transition systems and are hence not comparable to normal C programs. Tools relying on syntactic heuristics are hence at a disadvantage here.

We also have some coarse statistics about our examples:

	Average number	Mean number	Max number
Locations	24	9	468
Cutpoints	3	2	120
Transitions	37	11	807

Detailed Results

In our experiments, we used a timeout of 300 seconds for each example. We ran Terminator, T2 and Cooperating-T2 on a system using a quadcore 2.26GHz E5520 with 8GB of RAM and running Windows 7. The remaining tests were performed on a quadcore 3.07GHz Core i7 system with 4GB of RAM and running Debian Linux 6.

An overview of our results:

	Cooperating-T2	Terminator	T2	ARMC	AProVE	AProVE+Interproc	Size-Change/MCNP (AProVE)	KITTeL
Number TERM	245	177	189	138	197	185	156	196
Avg. time TERM (s)	3.42	4.99	5.15	16.16	2.21	1.53	17.50	4.65
Number NONTERM	174	181	180	0	0	0	0	0
Avg. time NONTERM (s)	1.68	5.88	6.67	0	0	0	0	0
Avg. time total (s)	13.77	52.60	47.61	68.61	47.23	81.30	82.81	129.30

In the following tables, results of our evaluation are detailed. Examples with differing results (i.e., TERMINATING vs. TIMEOUT) are highlighted with a yellow background: