No CrossRef data available.
Article contents
SAT-based termination analysis using monotonicity constraints over the integers
Published online by Cambridge University Press: 06 July 2011
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
We describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints in the integer domain. Monotonicity constraints are a nontrivial 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 (for “monotonicity constraints in NP”), 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. 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.
Information
- Type
- Regular Papers
- Information
- Theory and Practice of Logic Programming , Volume 11 , Special Issue 4-5: 27th International Conference on Logic Programming , July 2011 , pp. 503 - 520
- Copyright
- Copyright © Cambridge University Press 2011
References
Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G. and Zanardini, D. 2008. Termination analysis of Java Bytecode. In Proc. of the International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '08). Lecture Notes in Computer Science, vol. 5051. Springer-Verlag, Berlin, 2–18.CrossRefGoogle Scholar
Alias, C., Darte, A., Feautrier, P. and Gonnord, L. 2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proc. of the International Symposium on Static Analysis (SAS '10). Lecture Notes in Computer Science, vol. 6337. Springer-Verlag, Berlin, 117–133.Google Scholar
Avery, J. 2006. Size-change termination and bound analysis. In Proc. of the International Symposium on Functional and Logic Programming (FLOPS '06). Lecture Notes in Computer Science, vol. 3945. Springer-Verlag, Berlin, 192–207.CrossRefGoogle Scholar
Ben-Amram, A. M. 2009. A complexity tradeoff in ranking-function termination proofs. Acta Informatica 46 (1), 57–72.CrossRefGoogle Scholar
Ben-Amram, A. M. Monotonicity constraints for termination in the integer domain. Accepted for publication in Logical Methods of Computer Science. URL: http://arxiv.org/abs/1105.6317.Google Scholar
Ben-Amram, A. M. and Codish, M. 2008. A SAT-based approach to size-change termination with global ranking functions. In Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '08). Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, 218–232.Google Scholar
Ben-Amram, A. M. and Lee, C. S. 2007. Size-change analysis in polynomial time. ACM Transactions on Programming Languages and Systems 29 (1), 5:1–5:37.CrossRefGoogle Scholar
Brockschmidt, M., Otto, C., von Essen, C. and Giesl, J. 2010. Termination graphs for Java Bytecode. In Verification, Induction, Termination Analysis. Lecture Notes in Artificial Intelligence, vol. 6463. Springer-Verlag, Berlin, 17–37.CrossRefGoogle Scholar
Codish, M., Lagoon, V. and Stuckey, P. J. 2005. Testing for termination with monotonicity constraints. In Proc. of the International Conference on Logic Programming (ICLP '05). Lecture Notes in Computer Science, vol. 3668. Springer-Verlag, Berlin, 326–340.Google Scholar
Codish, M., Lagoon, V. and Stuckey, P. J. 2006. Solving partial order constraints for LPO termination. In Proc. of the International Conference on Rewriting Techniques and Applications (RTA '06). Lecture Notes in Computer Science, vol. 4098. Springer-Verlag, Berlin, 4–18.Google Scholar
Codish, M. and Taboch, C. 1999. A semantic basis for termination analysis of logic programs. Journal of Logic Programming 41 (1), 103–123.CrossRefGoogle Scholar
Colón, M. and Sipma, H. 2002. Practical methods for proving program termination. In Proc. of the International Conference on Computer Aided Verification (CAV '02). Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, 442–454.CrossRefGoogle Scholar
Dershowitz, N., Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 2001. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing 12 (1–2), 117–156.CrossRefGoogle Scholar
Dershowitz, N. and Manna, Z. 1979. Proving termination with multiset orderings. Communications of the ACM 22 (8), 465–476.CrossRefGoogle Scholar
Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P. and Falke, S. 2009. Proving termination of integer term rewriting. In Proc. of the International Conference on Rewriting Techniques and Applications (RTA '09). Lecture Notes in Computer Science, vol. 5595. Springer-Verlag, Berlin, 32–47.CrossRefGoogle Scholar
Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S. 2006. Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37 (3), 155–203.CrossRefGoogle Scholar
Giesl, J., Thiemann, R., Swiderski, S. and Schneider-Kamp, P. 2007. Proving termination by bounded increase. In Proc. of the International Conference on Automated Deduction (CADE '07). Lecture Notes in Artificial Intelligence, vol. 4603. Springer-Verlag, Berlin, 443–459.Google Scholar
Hirokawa, N. and Middeldorp, A. 2005. Automating the dependency pair method. Information and Computation 199 (1–2), 172–199.CrossRefGoogle Scholar
Le Berre, D. and Parrain, A. 2010. The SAT4J library, release 2.2, system description. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64.CrossRefGoogle Scholar
Lee, C. S., Jones, N. D. and Ben-Amram, A. M. 2001. The size-change principle for program termination. In Proc. of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '01). ACM Press, 81–92.Google Scholar
Lindenstrauss, N. and Sagiv, Y. 1997. Automatic termination analysis of Prolog programs. In Proc. of the International Conference on Logic Programming (ICLP '97). MIT Press, 64–77.Google Scholar
Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 2004. Proving termination for logic programs by the query-mapping pairs approach. In Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development. Lecture Notes in Computer Science, vol. 3049. Springer-Verlag, Berlin, 453–498.CrossRefGoogle Scholar
Manna, Z. and Waldinger, R. 1978. Is “sometime” sometimes better than “always”? Communications of the ACM 21, 159–172.CrossRefGoogle Scholar
Manolios, P. and Vroon, D. 2006. Termination analysis with calling context graphs. In Proc. of the International Conference on Computer-Aided Verification (CAV '06). Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, Berlin, 401–414.CrossRefGoogle Scholar
Otto, C., Brockschmidt, M., von Essen, C. and Giesl, J. 2010. Automated termination analysis of Java Bytecode by term rewriting. In Proc. of the International Conference on Rewriting Techniques and Applications (RTA '10). Leibniz International Proceedings in Informatics, vol. 6. Dagstuhl, Germany, 259–276.Google Scholar
Serebrenik, A. and De Schreye, D. 2004. Inference of termination conditions for numerical loops in Prolog. Theory and Practice of Logic Programming 4 (5–6), 719–751.CrossRefGoogle Scholar
Spoto, F., Mesnard, F. and Payet, E. 2010. A termination analyser for Java Bytecode based on path-length. ACM Transactions on Programming Languages and Systems 32 (3), 8:1–8:7.CrossRefGoogle Scholar
You have
Access
- 4
- Cited by