Skip to main content
SpringerLink
Log in

Synthesizing Nested Ranking Functions for Loop Programs via SVM

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2019)

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

Included in the following conference series:

Abstract

Termination of programs is probably the most famous undecidable problem in computer science. Despite this undecidability result, a lot of effort has been spent on improving algorithms that prove termination of loops, which is one of the building blocks of software reliability analysis. These algorithms are usually focused on finding an appropriate ranking function for the loop, which proves its termination. In this paper, we consider nested ranking functions for loop programs and show that the existence problem of a nested ranking function is equivalent to the existence problem of a hyperplane separating classes of data. This allows us to leverage Support-Vector Machines (SVM) techniques for the synthesis of nested ranking functions. SVM are supervised learning algorithms that are used to classify data; they work by finding a hyperplane separating data points parted into two classes. We show how to carefully define the data points so that the separating hyperplane gives rise to a nested ranking function for the loop. Experimental results confirm the effectiveness of our SVM-based synthesis of nested ranking functions.

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

Notes

  1. 1.

    https://sv-comp.sosy-lab.org/.

References

  1. Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP, pp. 229–238 (2013)

    Google Scholar 

  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: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 601–620. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_32

    Chapter  Google Scholar 

  4. Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 133–155. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_9

    Chapter  Google Scholar 

  5. Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_48

    Chapter  Google Scholar 

  6. Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349–1361. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_109

    Chapter  Google Scholar 

  7. Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 34–49. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_3

    Chapter  Google Scholar 

  8. Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_6

    Chapter  MATH  Google Scholar 

  9. Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_36

    Chapter  Google Scholar 

  10. Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)

    Article  Google Scholar 

  11. Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995)

    MATH  Google Scholar 

  12. Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_1

    Chapter  MATH  Google Scholar 

  13. Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional time. IJPP 21(5), 313–347 (1992)

    MathSciNet  MATH  Google Scholar 

  14. Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_26

    Chapter  MATH  Google Scholar 

  15. Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797–813. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_53

    Chapter  Google Scholar 

  16. Leike, J., Heizmann, M.: Ranking templates for linear loops. LMCS 11(1) (2015)

    Google Scholar 

  17. Leike, J., Heizmann, M.: Geometric nontermination arguments. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part II. LNCS, vol. 10806, pp. 266–283. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_16

    Chapter  Google Scholar 

  18. Li, Y., Zhu, G., Feng, Y.: The L-depth eventual linear ranking functions for single-path linear constraint loops. In: TASE, pp. 30–37 (2016)

    Google Scholar 

  19. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  20. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_20

    Chapter  Google Scholar 

  21. Shen, L., Wu, M., Yang, Z., Zeng, Z.: Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. J. Syst. Sci. Complex. 26(2), 291–301 (2013)

    Article  MathSciNet  Google Scholar 

  22. Smola, A.J., Schölkopf, B.: A tutorial on support vector regression. Stat. Comput. 14(3), 199–222 (2004)

    Article  MathSciNet  Google Scholar 

  23. Sohn, K., Gelder, A.V.: Termination detection in logic programs using argument sizes. In: PODS, pp. 216–226 (1991)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  25. Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem: a correction. Proc. Lond. Math. Soc. 2(42), 544–546 (1937)

    MathSciNet  MATH  Google Scholar 

  26. Yuan, Y., Li, Y.: Ranking function detection via SVM: a more general method. IEEE Access 7, 9971–9979 (2019)

    Article  Google Scholar 

Download references

Acknowledgement

This work is supported by the National Natural Science Foundation of China (Grants Nos. 61532019, 61761136011, 61572024), the Natural Science Foundation of Chongqing (Grant No. cstc2019jcyj-msxmX0638) and the Guangdong Science and Technology Department (Grant No. 2018B010107004).

Author information

Authors and Affiliations

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

    Yi Li

  2. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Xuechao Sun, Yong Li, Andrea Turrini & Lijun Zhang

  3. University of the Chinese Academy of Sciences, Beijing, China

    Xuechao Sun, Yong Li & Lijun Zhang

  4. Institute of Intelligent Software, Guangzhou, Guangzhou, China

    Andrea Turrini & Lijun Zhang

Authors
  1. Yi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xuechao Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrea Turrini
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Lijun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrea Turrini .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, Y., Sun, X., Li, Y., Turrini, A., Zhang, L. (2019). Synthesizing Nested Ranking Functions for Loop Programs via SVM. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation