基于不变式生成的循环停机性验证

A Proving the Termination of Loops Based on the Generation of Invariants

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。

Proving the termination of loops is a difficult part of program verification.Program invariants can describe the relations of program variables.Linear invariants can describe the linear relations of variables,and the relations of variables in the loops can be presented by loop invariants.By generating linear invariants and polynomial loop invariants,we transform proving the termination of loops to solving an optimization problem,then we present a practical framework of proving termination.Using the framework,the termination of loops can be proved automatically,and the complexity bounds of loops can be computed.The experimental results show the practicality of the method.