Sciweavers

Share
CORR
2011
Springer

SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

7 years 9 months ago
SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers
ibe 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 ing 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.
Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amra
Added 20 Aug 2011
Updated 20 Aug 2011
Type Journal
Year 2011
Where CORR
Authors Michael Codish, Igor Gonopolskiy, Amir M. Ben-Amram, Carsten Fuhs, Jürgen Giesl
Comments (0)
books