Proving Total Correctness of Loop Programs via Symbolic-Numeric Computation Method

摘要：

In this paper, we present a symbolicnumeric hybrid method, based on Sum-of-Squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. And Gauss-Newton refinement and rational vector recovery-are applied on the approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show that our method is more efficient in practice.

作者: Wang Lin Min Wu Zhengfeng Yang Zhenbing Zeng

作者单位: Shanghai Key Laboratory of Trustworthy Computing East China Normal University, Shanghai 200062, China

会议类型: 国际会议

会议名称: The Fourth International Conference on Mathematical Aspects of Computer and Information Sciences(第四届计算机与信息科学中的数学方法国际会议 MACIS 2011)

会议地点: 北京

会议语种:英文

页码: 149-161

在线出版日期: 2011-10-21（万方平台首次上网日期，不代表论文的发表时间）