Empirical Evaluation of "SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers"

In the paper "SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers" we describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a non-trivial extension of the well-known size-change termination method. While deciding termination for systems of monotonicity constraints is PSPACE complete, we focus on a well-defined and significant subset, which we call MCNP, designed to be amenable to a SAT-based solution. Our technique is based on the search for a global ranking function defined in terms of bounded differences between multisets of integer values. We describe the application of our approach as the back-end for the termination analysis of Java Bytecode (JBC). At the front-end, systems of monotonicity constraints are obtained by abstracting information, using two different termination analyzers: AProVE and COSTA. Preliminary results reveal that our approach provides a good trade-off between precision and cost of analysis.


In our experiments, we consider precision and performance of four termination prover configurations that work on various flavors of programs on the integer domain.

Benchmark Suites

To assess the impact of our contributions, we have created three benchmark suites: Suite 1, Suite 2, Suite 3 The second and the third suite both originate from Java Bytecode (JBC) programs from the termination problem data base (TPDB) used in the International Termination Competition of 2010. In this competition, the three termination analyzers AProVE, COSTA, and Julia competed against each other.

Settings and Experiments

In summary, the results of our experiments clearly demonstrate the good trade-off between power and speed of MCNP. We conclude that MCNP is a valuable contribution to the battery of techniques applied in state-of-the-art termination analyzers.