微信服务号

微信订阅号

2025年3月24日 8:03 星期一
首页 > 过刊浏览>2015年第26卷第2期 >297-304. DOI:10.13328/j.cnki.jos.004782
PDF HTML阅读 XML下载 导出引用 引用提醒
多分支单变量循环程序的终止性分析
作者:
基金项目:

国家自然科学基金(61103110); 重庆市科技攻关项目(cstc2012ggB40004, cstc2013jjys0002)


Termination Analysis of Multipath Loop Programs with One Variable
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [15]
    • |
  • 相似文献
    • | | |
  • 文章评论
    摘要:

    对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的.

    Abstract:

    Termination of multipath loop programs with one variable is analyzed in this paper. It demonstrates that under proper conditions, this kind of loops is non-terminate if and only if there exist fixed points. Especially, if the class of programs are polynomial, then under proper conditions, the termination of the programs is decidable over the reals.

    参考文献
    [1] Yang L, Zhou CC, Zhan NJ, Xia BC. Recent advances in program verification through computer algebra. Frontiers of Computer Science in China, 2012,4(1):1-16.[doi: 10.1007/s11704-009-0074-7]
    [2] Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011,54(5):88-98.[doi: 10. 1145/1941487.1941509]
    [3] Ben-Amram AM, Genaim S. On the linear ranking problem for integer linear-constraint loops. In: Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM, 2013. 51-62.[doi: 10.1145/2429069. 2429078]
    [4] Colón MA, Sipma HB. Practical methods for proving program termination. In: Brinksma E, Larsen KG, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2002. 227-240.[doi: 10.1007/3-540-45657-0_36]
    [5] Colón MA, Sipma HB. Synthesis of linear ranking functions. In: Margaria T, Wang Y, eds. Proc. of the 7th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. London: Springer-Verlag, 2001. 67-81.[doi: 10.1007/3-540-45319-9_6]
    [6] 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]
    [7] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In: Steffen B, Levi G, eds. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2004. 239-251.[doi: 10.1007/ 978-3-540-24622-0_20]
    [8] Chen YH, Xia BC, Yang L, Zhan NS, Zhou CC. Discovering non-linear ranking functions by solving semi-algebraic systems. In: Jones CB, Liu ZM, Woodcock J, eds. Proc. of the Theoretical Aspects of Computing (ICTAC 2007). Berlin, Heidelberg: Springer-Verlag, 2007. 34-49.[doi: 10.1007/978-3-540-75292-9_3]
    [9] Yang L, Zhan NJ, Xia BC, Zhou CC. Program verification by using DISCOVERER. In: Meyer B, Woodcock J, eds. Proc. of the Verified Software: Theories, Tools, Experiments. Berlin, Heidelberg: Springer-Verlag, 2008. 528-538.[doi: 10.1007/978-3-540-69149-5_58]
    [10] Cousot P. Proving program invariance and termination by parametric abstraction Langrangian relaxation and semidefinite programming. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2005. 1-24.[doi: 10.1007/978-3-540-30579-8_1]
    [11] Tiwari A. Termination of linear programs. In: Alur R, Peled DA, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2004. 70-82.[doi: 10.1007/978-3-540-27813-9_6]
    [12] Braverman M. Termination of integer linear programs. In: Ball T, Jones RB, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2006. 372-385.[doi: 10.1007/11817963_34]
    [13] Xia BC, Yang L, Zhan NJ, Zhang ZH. Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing, 2009,23(2):171-190.[doi: 10.1007/s00165-009-0144-5]
    [14] 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]
    [15] Bradley A, Manna Z, Sipma H. Termination of polynomial programs. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2005. 113-129.[doi: 10.1007/978-3-540-30579-8_8]
    相似文献
    引证文献
引用本文

李轶,李传璨,吴文渊.多分支单变量循环程序的终止性分析.软件学报,2015,26(2):297-304

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

京公网安备 11040202500063号