TY - JOUR
T1 - Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
AU - Lin, Wang
AU - Wu, Min
AU - Yang, Zhengfeng
AU - Zeng, Zhenbing
PY - 2014/4
Y1 - 2014/4
N2 - 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.
AB - 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.
KW - precondition generation
KW - semidefinite programming
KW - sum-of-squares relaxation
KW - symbolic computation
KW - total correctness
UR - https://www.scopus.com/pages/publications/84897959470
U2 - 10.1007/s11704-014-3150-6
DO - 10.1007/s11704-014-3150-6
M3 - 文章
AN - SCOPUS:84897959470
SN - 2095-2228
VL - 8
SP - 192
EP - 202
JO - Frontiers of Computer Science
JF - Frontiers of Computer Science
IS - 2
ER -