微信服务号

微信订阅号

2025-4-6- 8
Home > Archive>Volume 35, Issue 3, 2024 >1307-1320. DOI:10.13328/j.cnki.jos.006817
PDF HTML XML Export Cite reminder
Termination Analysis of Single-path Linear Constraint Loops
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [30]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    The ranking function method is the main method for the termination analysis of loops, and it indicates that loop programs can be terminated. In view of single-path linear constraint loop programs, this study presents a method to analyze the termination of the loops. Based on the calculation of the normal space of the increasing function, this method considers the calculation of the ranking function in the original program space as that in the subspace. Experimental results show that the method can effectively verify the termination of most loop programs in the existing literature.

    Reference
    [1] Turing AM. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 1937, s2-42(1):230-265.[doi:10.1112/plms/s2-42.1.230]
    [2] Turing AM. On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society, 1938, s2-43(1):544-546.[doi:10.1112/plms/s2-43.6.544]
    [3] Tiwari A. Termination of linear programs. In:Proc. of the 16th Int'l Conf. on Computer Aided Verification. Boston:Springer, 2004. 70-82.
    [4] Li Y. Witness to non-termination of linear programs. Theoretical Computer Science, 2017, 681:75-100.[doi:10.1016/j.tcs.2017.03.036]
    [5] Xia BC, Zhang ZH. Termination of linear programs with nonlinear constraints. Journal of Symbolic Computation, 2010, 45(11):1234-1249.[doi:10.1016/j.jsc.2010.06.006]
    [6] Liu J, Xu M, Zhan NJ, Zhao HJ. Discovering non-terminating inputs for multi-path polynomial programs. Journal of Systems Science and Complexity, 2014, 27(6):1286-1304.[doi:10.1007/s11424-014-2145-6]
    [7] Chen YF, Heizmann M, Lengál O, Li Y, Tsai MH, Turrini A, Zhang LJ. Advanced automata-based algorithms for program termination checking. ACM SIGPLAN Notices, 2018, 53(4):135-150.[doi:10.1145/3296979.3192405]
    [8] He F, Han JT. Termination analysis for evolving programs:An incremental approach by reusing certified modules. Proceedings of the ACM on Programming Languages, 2020, 4(OOPSLA):199.[doi:10.1145/3428267] (查阅所有网上资料, 不确定期号信息是否正确, 请联系作者确认)
    [9] Chatterjee K, Fu HF, Goharshady AK. Termination analysis of probabilistic programs through positivstellensatz's. In:Proc. of the 28th Int'l Conf. on Computer Aided Verification. Toronto:Springer, 2016. 3-22.
    [10] Xue B, Zhan NJ, Li YJ, Wang QY. Robust non-termination analysis of numerical software. In:Proc. of the 4th Int'l Symp. on Dependable Software Engineering. Theories, Tools, and Applications. Beijing:Springer, 2018. 69-88.
    [11] Colón M, Sipma HB. Synthesis of linear ranking functions. In:Proc. of the 7th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Genova:Springer, 2001. 67-81.
    [12] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In:Proc. of the 5th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Venice:Springer, 2004. 239-251.
    [13] Bagnara R, Mesnard F, Pescetti A, Zaffanella E. A new look at the automatic synthesis of linear ranking functions. Information and Computation, 2012, 215:47-67.[doi:10.1016/j.ic.2012.03.003]
    [14] Li Y, Wu WY, Feng Y. On ranking functions for single-path linear-constraint loops. International Journal on Software Tools for Technology Transfer, 2020, 22(6):655-666.[doi:10.1007/s10009-019-00549-9]
    [15] Bradley AR, Manna Z, Sipma HB. Linear ranking with reachability. In:Proc. of the 17th Int'l Conf. on Computer Aided Verification. Edinburgh:Springer, 2005. 491-504.
    [16] Bradley AR, Manna Z, Sipma HB. The polyranking principle. In:Proc. of the 32nd Int'l Colloquium on Automata, Languages and Programming. Lisbon:Springer, 2005. 1349-1361.
    [17] Alias C, Darte A, Feautrier P, Gonnord L. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In:Proc. of the 17th Int'l Symp. on Static Analysis. Perpignan:Springer, 2010. 117-133.
    [18] Bagnara R, Mesnard F. Eventual linear ranking functions. In:Proc. of the 15th Symp. on Principles and Practice of Declarative Programming. Madrid:ACM. 2013. 229-238.
    [19] Li Y, Zhu G, Feng Y. The L-depth eventual linear ranking functions for single-path linear constraint lo扯異杳献攠湉杮?捐潲浯?瀮瀠汯?戠牴?孥??崰??漠浉敮湴攧捬栠??????敯湮愠楔浨?卯???ど????桁瑳瑰灥獣???杯楦琠桓畯扦?捷潡浲?挠潅獮瑧慩?来牥潲畩灮?椮删慓湨歡?楧湨摡敩爺?扅牅?, 2016. 30-37.
    [20] Leike J, Heizmann M. Ranking templates for linear loops. Logical Methods in Computer Science, 2015, 11(1):1-27. (查阅所有网上资料, 不确定期号和页码信息是否正确, 请联系作者确认)
    [21] Ben-Amram AM, Genaim S. On multiphase-linear ranking functions. In:Proc. of the 29th Int'l Conf. on Computer Aided Verification. Heidelberg:Springer, 2017. 601-620.
    [22] Yuan Y, Li Y, Shi WC. Detecting multiphase linear ranking functions for single-path linear-constraint loops. International Journal on Software Tools for Technology Transfer, 2021, 23(1):55-67.[doi:10.1007/s10009-019-00527-1]
    [23] Chen YH, Xia BC, Yang L, Zhan NJ, Zhou CC. Discovering non-linear ranking functions by solving semi-algebraic systems. In:Proc. of the 4th Int'l Colloquium on Theoretical Aspects of Computing. Macao:Springer, 2007. 34-49.
    [24] Cousot P. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In:Proc. of the 6th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Paris:Springer, 2005. 1-24.
    [25] Shen LY, Wu M, Yang ZF, Zeng ZB. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. Journal of Systems Science and Complexity, 2013, 26(2):291-301.[doi:10.1007/s11424-013-1004-1]
    [26] Li Y, Sun XC, Li Y, Turrini A, Zhang LJ. Synthesizing nested ranking functions for loop programs via SVM. In:Proc. of the 21st Int'l Conf. on Formal Engineering Methods. Shenzhen:Springer, 2019. 438-454.
    [27] 孙学超. 基于SVM算法的循环程序的终止性证明[硕士学位论文]. 北京:中国科学院大学, 2020.
    Sun XC. Proving the termination of loop programs based on SVM[MS. Thesis]. Beijing:University of Chinese Academy of Sciences, 2020 (in Chinese with English abstract).
    [28] Ben-Amram AM, Genaim S. Ranking functions for linear-constraint loops. Journal of the ACM, 2014, 61(4):1-55.[doi:10.1145/2629488]
    [29] Bagnara R, Hill PM, Zaffanella E. 2008. https://www.bugseng.com/pplhttp://www.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

李轶,唐桐.单分支线性约束循环程序的终止性分析.软件学报,2024,35(3):1307-1320

Copy
Share
Article Metrics
  • Abstract:343
  • PDF: 1803
  • HTML: 828
  • Cited by: 0
History
  • Received:March 01,2022
  • Revised:May 01,2022
  • Online: June 07,2023
  • Published: March 06,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033315Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063