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

被引：0

作者：

Wang Lin

Min Wu

Zhengfeng Yang

Zhenbing Zeng

机构：

[1] East China Normal University,Shanghai Key Laboratory of Trustworthy Computing

[2] Wenzhou University,College of Mathematics and Information Science

[3] Shanghai University,Department of Mathematics

来源：

Frontiers of Computer Science | 2014年 / 8卷

关键词：

symbolic computation; sum-of-squares relaxation; semidefinite programming; total correctness; precondition generation;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

We present a symbolic-numeric 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. The SOS relaxation method is used to compute approximate invariants and approximate ranking 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 examples are given to show the effectiveness of our method.

引用

页码：192 / 202

页数：10