Details on the implementation, and the sources of the tool, can be found on the T2 website.
We compare the following tools:
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|
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:
|Avg. time TERM (s)||3.42||4.99||5.15||16.16||2.21||1.53||17.50||4.65|
|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: