Advertisement

Synthesizing Nested Ranking Functions for Loop Programs via SVM

  • Yi Li
  • Xuechao Sun
  • Yong Li
  • Andrea TurriniEmail author
  • Lijun Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

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.

Notes

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

References

  1. 1.
    Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP, pp. 229–238 (2013)Google Scholar
  2. 2.
    Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1–26:55 (2014)MathSciNetCrossRefGoogle Scholar
  3. 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_32CrossRefGoogle Scholar
  4. 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_9CrossRefGoogle Scholar
  5. 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_48CrossRefGoogle Scholar
  6. 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_109CrossRefGoogle Scholar
  7. 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_3CrossRefGoogle Scholar
  8. 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_6CrossRefzbMATHGoogle Scholar
  9. 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_36CrossRefGoogle Scholar
  10. 10.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)CrossRefGoogle Scholar
  11. 11.
    Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995)zbMATHGoogle Scholar
  12. 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_1CrossRefzbMATHGoogle Scholar
  13. 13.
    Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional time. IJPP 21(5), 313–347 (1992)MathSciNetzbMATHGoogle Scholar
  14. 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_26CrossRefzbMATHGoogle Scholar
  15. 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_53CrossRefGoogle Scholar
  16. 16.
    Leike, J., Heizmann, M.: Ranking templates for linear loops. LMCS 11(1) (2015)Google Scholar
  17. 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 CrossRefGoogle Scholar
  18. 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. 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_24CrossRefGoogle Scholar
  20. 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_20CrossRefGoogle Scholar
  21. 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)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Smola, A.J., Schölkopf, B.: A tutorial on support vector regression. Stat. Comput. 14(3), 199–222 (2004)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Sohn, K., Gelder, A.V.: Termination detection in logic programs using argument sizes. In: PODS, pp. 216–226 (1991)Google Scholar
  24. 24.
    Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 2(42), 230–265 (1937)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem: a correction. Proc. Lond. Math. Soc. 2(42), 544–546 (1937)MathSciNetzbMATHGoogle Scholar
  26. 26.
    Yuan, Y., Li, Y.: Ranking function detection via SVM: a more general method. IEEE Access 7, 9971–9979 (2019)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Chongqing Key Laboratory of Automated Reasoning and Cognition, Automated Reasoning and Cognition CenterChongqing Institute of Green and Intelligent Technology, Chinese Academy of SciencesChongqingChina
  2. 2.State Key Laboratory of Computer ScienceInstitute of Software, Chinese Academy of SciencesBeijingChina
  3. 3.University of the Chinese Academy of SciencesBeijingChina
  4. 4.Institute of Intelligent Software, GuangzhouGuangzhouChina

Personalised recommendations