Abstract:

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.

Key words: invariant;proving termination;optimization problem;complexity bound