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

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
原文传递
导出
摘要 我们在场一个符号数字的混合方法，基于 sum-of-squares (求救) 松驰和合理向量恢复，为证明正确性全部并且为程序产生前提计算不平等 invariants 和评价函数。求救松驰方法被用来计算近似 invariants 并且接近与浮点系数评价功能。然后，高斯牛顿精炼和合理向量恢复被用于近似多项式与合理系数获得候选人多项式，它确切满足 invariants 的条件，评价工作。最后，几个例子被给显示出我们的方法的有效性。 We present a symbolic-numeric hybrid method, based on sum-of-squares （SOS） relaxation and rational vec- tor recovery, to compute inequality invariants and ranking functions for proving total correctness and generating pre- conditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate rank- ing functions with floating point coefficients. Then Gauss- Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several exam- ples are given to show the effectiveness of our method.
作者 Wang LIN Min WU Zhengfeng YANG Zhenbing ZENG
机构地区 Shanghai Key Laboratory of Trustworthy Computing College of Mathematics and Information Science Department of Mathematics
出处 《Frontiers of Computer Science》 SCIE EI CSCD 2014年第2期192-202,共11页 中国计算机科学前沿（英文版）
关键词 数值计算方法 循环程序 证明 不变量 混合方法 排序功能 SOS 松弛法 symbolic computation, sum-of-squares relax-ation, semidefinite programming, total correctness, precon-dition generation.
分类号 TP311.1 [自动化与计算机技术—计算机软件与理论] TM341 [电气工程—电机]
  • 相关文献

参考文献1

二级参考文献21

  • 1Turing A, On computable numbers, with an application to the entscheidungsproblem, Proc. of the London Mathematical Society, 1937, $2-42(1): 230-265.
  • 2Tiwari A, Termination of linear programs, Computer Aided Verification (ed. by Alur R and Peled D), Springer-Verlag, Lecture Notes in Computer Science, 2004, 3114: 70-82.
  • 3Braverman M, Termination of integer linear programs, Computer Aided Verification (ed. by Ball T and Jones R B), Springer-Verlag, Lecture Notes in Computer Science, 2006 4144: 372-385.
  • 4Bradley A R, Manna Z, and Sipma H B, Termination of polynomial programs, Verification, Model Checking, and Abstract Interpretation (ed. by Cousot R), Springer, Lecture Notes in Computer Science, 2005, 3385:113 129.
  • 5Babic D, Hu A J, Rakamaric Z, and Cook engineering and formal methods, IEEE, 2007, B, Proving termination by divergence: Software 93-102.
  • 6ColSn M and Sipma H B, Synthesis of linear ranking functions, Tools and Algorithms for the Construction and Analysis of Systems (ed. by Margaria T and Yi W), Springer-Verlag, Lecture Notes in Computer Science, 2001, 2031: 67-81.
  • 7Col6n M and Sipma H B, Practical methods for proving program termination, Computer Aided Verification (ed. by Brinksma E and Larsen K G), Springer-Verlag, Lecture Notes in Computer Science, 2002, 2404: 442-454.
  • 8Podelski A and Rybalchenko A, A complete method for the synthesis of linear ranking functions, Verification, Model Checking, and Abstract Interpretation (ed. by Steffen B and Levi G), Springer, Lecture Notes in Computer Science, 2004, 2937:239- 251.
  • 9Bradley A R, Manna Z, and Sipma H B, Termination analysis of integer linear loops, Concurrency Theory, 16th International Conference, Springer-Verlag, Lecture Notes in Computer Science, 2005, 3653: 488-502.
  • 10Chen Y, Xia B, Yang L, Zhan N, and Zhou C, Discovering non-linear ranking functions by solving semi-algebraic systems, Theoretical Aspects of Computing, Springer-Verlag, Lecture Notes in Computer Science, 2007, 4711: 34-49.

共引文献7

Frontiers of Computer Science
2014年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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