微信服务号

微信订阅号

2025年6月15日 16:43 星期日
首页 > 过刊浏览>2024年第35卷第3期 >1307-1320. DOI:10.13328/j.cnki.jos.006817
PDF HTML阅读 XML下载 导出引用 引用提醒
单分支线性约束循环程序的终止性分析
作者:
中图分类号:

TP311

基金项目:

重庆市自然科学基金(cstc2019jcyj-msxmX0638);国家自然科学基金(11771421);中国科学院“西部之光”人才培养计划


Termination Analysis of Single-path Linear Constraint Loops
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [30]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.

    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.

    参考文献
    [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.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:356
  • 下载次数: 1877
  • HTML阅读次数: 963
  • 引用次数: 0
历史
  • 收稿日期:2022-03-01
  • 最后修改日期:2022-05-01
  • 在线发布日期: 2023-06-07
  • 出版日期: 2024-03-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第20052370位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号