Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Book cover Static Analysis (SAS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11002))

Included in the following conference series:

  • 944 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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)

    Article  MathSciNet  Google Scholar 

  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_8

    Chapter  Google Scholar 

  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_9

    Chapter  Google Scholar 

  4. Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3), 1–30 (2008)

    Google Scholar 

  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. Blass, A., Gurevich, Y.: Program termination and well partial orderings. ACM Trans. Comput. Log. 9(3), 18:1–18:26 (2008)

    MathSciNet  MATH  Google Scholar 

  7. Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: VMCAI, pp. 88–103 (2012)

    Google Scholar 

  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_28

    Chapter  Google Scholar 

  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_16

    Chapter  MATH  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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_20

    Chapter  Google Scholar 

  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_18

    Chapter  Google Scholar 

  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_1

    Chapter  Google Scholar 

  14. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415–426 (2006)

    Google Scholar 

  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_4

    Chapter  Google Scholar 

  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_15

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  18. Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292–304 (2010)

    Google Scholar 

  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_4

    Chapter  Google Scholar 

  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_34

    Chapter  Google Scholar 

  21. Lee, C.S.: Ranking functions for size-change termination. ACM Trans. Program. Lang. Syst. 31(3), 10:1–10:42 (2009)

    Article  Google Scholar 

  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. 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_36

    Chapter  Google Scholar 

  24. Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006)

    Article  MathSciNet  Google Scholar 

  25. Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41 (2004)

    Google Scholar 

  26. Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), 15 (2007)

    Article  Google Scholar 

  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. Simon, I.: Factorization forests of finite height. Theor. Comput. Sci. 72(1), 65–94 (1990)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  30. Steila, S., Yokoyama, K.: Reverse mathematical bounds for the termination theorem. Ann. Pure Appl. Logic 167(12), 1213–1241 (2016)

    Article  MathSciNet  Google Scholar 

  31. Vidal, G.: Quasi-terminating logic programs for ensuring the termination of partial evaluation. In: PEPM, pp. 51–60 (2007)

    Google Scholar 

  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_17

    Chapter  Google Scholar 

  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_27

    Chapter  Google Scholar 

  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_22

    Chapter  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Florian Zuleger

Authors
  1. Florian Zuleger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florian Zuleger .

Editor information

Editors and Affiliations

  1. Universität Freiburg, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zuleger, F. (2018). Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99725-4_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99724-7

  • Online ISBN: 978-3-319-99725-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation