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

被引：3

作者：

Lin, Wang ^{[1
,2
]}

Wu, Min ^{[1
]}

Yang, Zhengfeng ^{[1
]}

Zeng, Zhenbing ^{[3
]}

机构：

[1] E China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China

[2] Wenzhou Univ, Coll Math & Informat Sci, Wenzhou 325035, Zhejiang, Peoples R China

[3] Shanghai Univ, Dept Math, Shanghai 200444, Peoples R China

来源：

FRONTIERS OF COMPUTER SCIENCE | 2014年 / 8卷 / 02期

基金：

国家高技术研究发展计划(863计划); 中国国家自然科学基金;

关键词：

symbolic computation; sum-of-squares relaxation; semidefinite programming; total correctness; precondition generation; NONLINEAR RANKING FUNCTIONS; POLYNOMIAL INVARIANTS; VERIFICATION; TERMINATION;

D O I：

10.1007/s11704-014-3150-6

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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

页数：11