A SAT-Based Approach to Size Change Termination with Global Ranking Functions

  • Amir M. Ben-Amram
  • Michael Codish
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


We describe a new approach to proving termination with size change graphs. This is the first decision procedure for size change termination (SCT) which makes direct use of global ranking functions. It handles a well-defined and significant subset of SCT instances, designed to be amenable to a SAT-based solution. We have implemented the approach using a state-of-the-art Boolean satisfaction solver. Experimentation indicates that the approach is a viable alternative to the complete SCT decision procedure based on closure computation and local ranking functions. Our approach has the extra benefit of producing an explicit witness to prove termination in the form of a global ranking function.


Logic Programming Ranking Function Level Mapping Propositional Variable Satisfying Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Avery, J.: Size-change termination and bound analysis. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Ben-Amram, A.M.: A complexity tradeoff in ranking-function termination proofs (submitted for publication 2007)Google Scholar
  3. 3.
    Ben-Amram, A.M., Lee, C.S.: Ranking functions for size-change termination II. In: 9th International Workshop on Termination (WST 2007) (July 2007)Google Scholar
  4. 4.
    Ben-Amram, A.M., Lee, C.S.: Size-change analysis in polynomial time. ACM Transactions on Programming Languages and Systems 29(1) (2007)Google Scholar
  5. 5.
    Bruynooghe, M., Codish, M., Gallagher, J.P., Genaim, S., Vanhoof, W.: Termination analysis of logic programs through combination of type-based norms. ACM TOPLAS 29(2) (2007)Google Scholar
  6. 6.
    Codish, M., Lagoon, V., Stuckey, P.J.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 326–340. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Codish, M., Lagoon, V., Stuckey, P.J.: Logic programming with satisfiability. Theory and Practice of Logic Programming (2007)Google Scholar
  8. 8.
    Codish, M., Taboch, C.: A semantic basis for termination analysis of logic programs. The Journal of Logic Programming 41(1), 103–123 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Codish, M., Lagoon, V., Stuckey, P.J.: Solving partial order constraints for LPO termination. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 4–18. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87–101. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M., Ball, T. (eds.) Proc. PLDI, pp. 415–426. ACM Press, New York (2006)Google Scholar
  12. 12.
    Lee, C.S.: Ranking functions for size-change termination (submitted 2007)Google Scholar
  13. 13.
    Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing 12(1–2), 117–156 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Jones, N.D., Bohr, N.: Termination analysis of the untyped lambda calculus. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 1–23. Springer, Heidelberg (2004)Google Scholar
  16. 16.
    Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460–475. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL 2001, January 2001, vol. 28, pp. 81–92. ACM Press, New York (2001)Google Scholar
  18. 18.
    Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: Termilog: A system for checking termination of queries to logic programs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 444–447. Springer, Heidelberg (1997)Google Scholar
  19. 19.
    Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 401–414. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    MiniSAT solver (Viewed December 2005),
  21. 21.
    Necula, G.C.: Proof-carrying code. In: Proc. POPL, pp. 106–119. ACM Press, New York (1997)Google Scholar
  22. 22.
    Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and sat solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 267–282. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Sereni, D., Jones, N.: Termination analysis of higher-order functional programs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 281–297. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  24. 24.
    Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing 16(4), 229–270 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    The termination problem data base.

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Amir M. Ben-Amram
    • 1
  • Michael Codish
    • 2
  1. 1.School of Computer ScienceTel-Aviv Academic CollegeIsrael
  2. 2.Department of Computer ScienceBen-Gurion UniversityIsrael

Personalised recommendations