SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

Details SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers

2011-07-29

arxiv.org/abs/1107.5980v1

Theory and Practice of Logic Programming, 27th International Conference on Logic Programming (ICLP'11) Special Issue, volume 1

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-319180