SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

TL;DR

This paper presents a SAT-based algorithm for proving program termination using monotonicity constraints over integers, extending size-change termination methods and applied to Java Bytecode analysis.

Contribution

It introduces a SAT-based approach for termination analysis with monotonicity constraints, focusing on a tractable subset called MCNP, and demonstrates its application to Java Bytecode.

Findings

Effective trade-off between analysis precision and cost.

Applicable to Java Bytecode via abstraction from existing analyzers.

Preliminary results show promising performance.

Abstract

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 special type of 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.