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

作　　者：Wang LIN Min WU Zhengfeng YANG Zhenbing ZENG 

机构地区：[1]Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China [2]College of Mathematics and Information Science, Wenzhou University, Zhejiang 325035, China [3]Department of Mathematics, Shanghai University, Shanghai 200444, China

出　　处：《Frontiers of Computer Science》2014年第2期192-202,共11页中国计算机科学前沿（英文版）

摘　　要：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.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.

关 键 词：symbolic computation sum-of-squares relax-ation semidefinite programming total correctness precon-dition generation. 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论] TM341[自动化与计算机技术—计算机科学与技术]