Skip to main content
SpringerLink
Log in

Detecting multiphase linear ranking functions for single-path linear-constraint loops

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Single-path linear-constraint loops are important since many analyses in different fields can be reduced to termination proof synthesis for such loops. In 2017, Ben-Amram and Genaim provided a complete polynomial-time solution to the problem of existence and of synthesis of multiphase linear ranking functions (\(M\varPhi \hbox {RFs}\)) of bounded depth to prove the termination of a single-path linear-constraint loop. However, an open question whether one can precompute a bound on the depth of a \(M\varPhi \hbox {RF}\) for a given loop is raised and the solution has not been accomplished so far. In this paper, we propose an approach to depth bound detection and synthesis of \(M\varPhi \hbox {RFs}\) for rational single-path linear-constraint loops. We take a step further based on the work of Ben-Amram and Genaim, and detect the depth bound for a certain class of rational single-path linear-constraint loops. Furthermore, the effectiveness of our approach is presented with experimental evidence. The depth bound can be precomputed for loops where existing tools fail to infer a \(M\varPhi \hbox {RF}\) or prove that none exists.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: In Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, pp. 229–238. ACM Press (2013)

  2. Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1–26:55 (2014)

    Article  MathSciNet  Google Scholar 

  3. Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: International Conference on Computer Aided Verification, pp. 601–620. Springer International Publishing, Cham (2017)

  4. Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Computer Aided Verification, pp. 491–504. Springer, Berlin (2005)

  5. Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Proceedings of the 32nd International Conference on Automata, Languages and Programming, ICALP’05, pp. 1349–1361. Springer, Berlin (2005)

  6. Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. Int. J. Softw. Tools Technol. Transf. 17(1), 47–57 (2015)

    Article  Google Scholar 

  7. Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: Theoretical Aspects of Computing—ICTAC 2007, pp. 34–49. Springer, Berlin (2007)

  8. Chen, Y.-F., Heizmann, M., Lengál, O., Li, Y., Tsai, M.-H., Turrini, A., Zhang, L.: Advanced automata-based algorithms for program termination checking. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 135–150. ACM (2018)

  9. Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, pp. 67–81. Springer (2001)

  10. Colón, M., Sipma, H.: Practical methods for proving program termination. In: Proceedings of the 14th International Conference on Computer Aided Verification, CAV ’02, pp. 442–454. Springer (2002)

  11. Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’07, pp. 265–276. ACM (2007)

  12. Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Proceedings of the 20th International Conference on Computer Aided Verification, CAV ’08, pp. 328–340. Springer, Berlin (2008)

  13. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’06, pp. 415–426. ACM (2006)

  14. Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI’05, pp. 1–24. Springer, Berlin (2005)

  15. Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: International Conference on Computer Aided Verification, pp. 124–143. Springer International Publishing, Cham (2018)

  16. Ganty, P., Genaim, S.: Proving termination starting from the end. In: International Conference on Computer Aided Verification, pp. 397–412. Springer, Berlin (2013)

  17. Larraz, D., Oliveras, A., Enric R.-C., Albert R.: Proving termination of imperative programs using MAX-SMT. In: Formal Methods in Computer-Aided Design, pp. 218–225 (2014)

  18. Leike, J., Heizmann, M.: Ranking templates for linear loops. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 172–186. Springer, Berlin (2014)

  19. Leike, J., Heizmann, M.: Geometric nontermination arguments. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 266–283. Springer International Publishing, Cham (2018)

  20. Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: In International Symposium on Automated Technology for Verification and Analysis, pp. 489–503. Springer, Berlin (2005)

  21. Li, Y.: Termination of semi-algebraic loop programs. In: International Symposium on Dependable software Engineering: Theories, Tools and Applications (SETTA’17), pp. 131–146. Springer (2017)

  22. Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75–100 (2017)

    Article  MathSciNet  Google Scholar 

  23. Li, Y., Zhu, G., Feng, Y.: The l-depth eventual linear ranking functions for single-path linear constraint loops. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 30–37. IEEE (2016)

  24. Ouaknine, J., Worrell, J.: On linear recurrence sequences and loop termination. ACM SIGLOG News 2(2), 4–13 (2015)

    Article  Google Scholar 

  25. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Verification, Model Checking, and Abstract Interpretation, pp. 239–251. Springer, Berlin (2004)

  26. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)

    MATH  Google Scholar 

  27. Turing, A.M.: On computable numbers, with an application to the entscheidungs problem. Proc Lond. Math. Soc. 42(2), 230–265 (1937)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information, Renmin University of China, Beijing, 100872, China

    Yue Yuan & Wenchang Shi

  2. Chongqing Key Laboratory of Automated Reasoning and Cognition, Automated Reasoning and Cognition Center, Chongqing Institute of Green and Intelligent Technology, The Chinese Academy of Sciences, Chongqing, 401120, China

    Yi Li

Authors
  1. Yue Yuan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wenchang Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yi Li.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work was supported in part by the National Nature Science Foundation of China under Grant Nos. (61070192, 61572024, 61103110, 61472429, 91018008, 61303074, 61170240), Beijing Nature Science Foundation under Grant No. 4122041, National HighTech Research Development Program of China under Grant No. 2007AA01Z414, National Science and Technology Major Project of China under Grant No. 2012ZX01039-004, and Natural Science Foundation of Chongqing under Grant No. cstc2019jcyjAX0982.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Yuan, Y., Li, Y. & Shi, W. Detecting multiphase linear ranking functions for single-path linear-constraint loops. Int J Softw Tools Technol Transfer 23, 55–67 (2021). https://doi.org/10.1007/s10009-019-00527-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-019-00527-1

Keywords

Search

Navigation