SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amram +2

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 ext…