GENERATING EXACT NONLINEAR RANKING FUNCTIONS BY SYMBOLIC-NUMERIC HYBRID METHOD

作     者：SHEN Liyong WU Min YANG Zhengfeng ZENG Zhenbing 

作者机构：School of Mathematical SciencesGraduate University of Chinese Academy of Sciences Shanghai Key Laboratory of Trustworthy ComputingEast China Normal University 

出 版 物：《Journal of Systems Science & Complexity》 (系统科学与复杂性学报（英文版）)

年 卷 期：2013年第26卷第2期

页      面：291-301页

核心收录：

学科分类：080904[工学-电磁场与微波技术] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：supported in part by the National Natural Science Foundation of China under Grant Nos.10901055,61021004,91118007 by NKBRPC 2011CB302802,2011CB70690 by the Fundamental Research Funds for the Central Universities under Grant No.78210043 

主　　题：Program verification ranking function semidefinite programming symbolic-numeric hybrid method. 

摘      要：This paper presents a hybrid symbolic-numeric algorithm to compute ranking functions for establishing the termination of loop programs with polynomial guards and polynomial *** authors first transform the problem into a parameterized polynomial optimization problem,and obtain a numerical ranking function using polynomial sum-of-squares relaxation via semidefinite programming(SDP).A rational vector recovery algorithm is deployed to recover a rational polynomial from the numerical ranking function,and some symbolic computation techniques are used to certify that this polynomial is an exact ranking function of the loop *** last,the authors demonstrate on some polynomial loop programs from the literature that our algorithm successfully yields nonlinear ranking functions with rational coefficients.