期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

多分支单变量循环程序的终止性分析

Termination Analysis of Multipath Loop Programs with One Variable
下载PDF
导出
摘要 对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的. 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.
作者 李轶 李传璨 吴文渊
机构地区 自动推理与认知重庆市重点实验室(中国科学院重庆绿色智能技术研究院) 重庆邮电大学计算机科学与技术学院
出处 《软件学报》 EI CSCD 北大核心 2015年第2期297-304,共8页 Journal of Software
基金 国家自然科学基金(61103110) 重庆市科技攻关项目(cstc2012gg B40004 cstc2013jjys0002)
关键词 可信计算 多分支循环程序 终止性分析 trusted computing multipath loop program termination analysis
分类号 TP311 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献15

  • 1Yang 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/s 11704-009-0074-7].
  • 2Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011,54(5):88-98. [doi: 10. 1145/1941487.1941509].
  • 3Ben-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].
  • 4Col6n 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].
  • 5Col6n 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].
  • 6Bagnara 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.ie.2012.03.003].
  • 7Podelski 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].
  • 8Chen 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].
  • 9Yang 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: Spriuger-Verlag, 2008. 528-538. Idol: 10.1007/978-3-540- 69149-5_58].
  • 10Cousot 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].
软件学报
2015年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部