Advertisement

Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction

  • Florian ZulegerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Transition invariants are a popular technique for automated termination analysis. A transition invariant is a covering of the transitive closure of the transition relation of a program by a finite number of well-founded relations. The covering is usually established by an inductive proof using transition predicate abstraction. Such inductive termination proofs have the structure of a finite automaton. These automata, which we call transition automata, offer a rich structure that has not been exploited in previous publications. We establish a new connection between transition automata and the size-change abstraction, which is another widespread technique for automated termination analysis. In particular, we are able to transfer recent results on automated complexity analysis with the size-change abstraction to transition invariants.

Notes

Acknowledgements

This article is dedicated to the memory of Helmut Veith who proposed to me the PhD topic of automatic derivation of loop bounds. Our initial idea was to extend the termination analysis of Terminator. With this article I managed to return to this original idea.

References

  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142–159 (2012)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117–133. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_8CrossRefGoogle Scholar
  3. 3.
    Anderson, H., Khoo, S.-C.: Affine-based size-change termination. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 122–140. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-40018-9_9CrossRefGoogle Scholar
  4. 4.
    Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3), 1–30 (2008)Google Scholar
  5. 5.
    Ben-Amram, A.M.: Monotonicity constraints for termination in the integer domain. Log. Methods Comput. Sci. 7(3), 1–43 (2011)Google Scholar
  6. 6.
    Blass, A., Gurevich, Y.: Program termination and well partial orderings. ACM Trans. Comput. Log. 9(3), 18:1–18:26 (2008)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: VMCAI, pp. 88–103 (2012)Google Scholar
  8. 8.
    Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_28CrossRefGoogle Scholar
  9. 9.
    Codish, M., Fuhs, C., Giesl, J., Schneider-Kamp, P.: Lazy abstraction for size-change termination. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 217–232. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16242-8_16CrossRefzbMATHGoogle Scholar
  10. 10.
    Codish, M., Gonopolskiy, I., Ben-Amram, A.M., Fuhs, C., Giesl, J.: Sat-based termination analysis using monotonicity constraints over the integers. TPLP 11(4–5), 503–520 (2011)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Colcombet, T.: Factorisation forests for infinite words. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 226–237. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74240-1_20CrossRefGoogle Scholar
  12. 12.
    Colcombet, T., Daviaud, L., Zuleger, F.: Size-change abstraction and max-plus automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 208–219. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44522-8_18CrossRefGoogle Scholar
  13. 13.
    Colcombet, T., Daviaud, L., Zuleger, F.: Automata and program analysis. In: Klasing, R., Zeitoun, M. (eds.) FCT 2017. LNCS, vol. 10472, pp. 3–10. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-55751-8_1CrossRefGoogle Scholar
  14. 14.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415–426 (2006)Google Scholar
  15. 15.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_4CrossRefGoogle Scholar
  16. 16.
    Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-12736-1_15CrossRefGoogle Scholar
  17. 17.
    Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with aprove. J. Autom. Reason. 58(1), 3–31 (2017)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292–304 (2010)Google Scholar
  19. 19.
    Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 22–50. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_4CrossRefGoogle Scholar
  20. 20.
    Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 460–475. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73595-3_34CrossRefGoogle Scholar
  21. 21.
    Lee, C.S.: Ranking functions for size-change termination. ACM Trans. Program. Lang. Syst. 31(3), 10:1–10:42 (2009)CrossRefGoogle Scholar
  22. 22.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81–92 (2001)Google Scholar
  23. 23.
    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).  https://doi.org/10.1007/11817963_36CrossRefGoogle Scholar
  24. 24.
    Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41 (2004)Google Scholar
  26. 26.
    Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), 15 (2007)CrossRefGoogle Scholar
  27. 27.
    Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP, pp. 53–65 (2017)Google Scholar
  28. 28.
    Simon, I.: Factorization forests of finite height. Theor. Comput. Sci. 72(1), 65–94 (1990)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3–45 (2017)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Steila, S., Yokoyama, K.: Reverse mathematical bounds for the termination theorem. Ann. Pure Appl. Logic 167(12), 1213–1241 (2016)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Vidal, G.: Quasi-terminating logic programs for ensuring the termination of partial evaluation. In: PEPM, pp. 51–60 (2007)Google Scholar
  32. 32.
    Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full: adventures in constructive termination. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250–265. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32347-8_17CrossRefGoogle Scholar
  33. 33.
    Zuleger, F.: Asymptotically precise ranking functions for deterministic size-change systems. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 426–442. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-20297-6_27CrossRefGoogle Scholar
  34. 34.
    Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_22CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.TU WienViennaAustria

Personalised recommendations