Study On Program Verification

Program verification is the key method for ensuring correctness of programs. As two important parts of program verification, termination proving and safety verification receive more and more attentions.This thesis performs a systematic and deep study of theories and algorithms for termination proving and safety verification. Main contributions of this thesis can be summarized as follows:1. Base on the optimization problems, we present a method for generating linear ranking functions. Firstly, templates of linear ranking functions and a preset range of parameters are given. Secondly, unknown coefficients of templates are replaced by a value of the range. Then considering loop invariants as constraint system and differences of instantiation of linear ranking functions'templates as objective function, we construct an optimization problem. The optimal solution of the optimization problem which is the minimal decending step of ranking functions can be used to compute accurate complexity bound of program. This method for generating linear ranking functions can handle not only linear and polynomial programs but also some programs with exponents and logarithms.2. We present a framework of termination proving and safety verification by generation of invariants. Invariants are used as constraint systems of program variables. By instrumenting a counter into loops, we can transform the termination problem into an optimization problem. The constraint system of the optimization problem is the invariants'set at the exit of the loop. The objective function is computing the minimal value of the loop counter. Using this method, ranking functions are no longer needed and termination of some programs without ranking fuctions can also ben proved. We also present a method of verifying safety by proving a logical formula using theorem prover. The logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. Because invariants are generated at any control point of a program, weakest preconditions are no longer needed. Compared with methods computing weakest preconditions, our method can be automated more easily.3. Based on the solving techniques of recurrence equations and optimization problems, we present a practical approach for computing symbolic complexity bounds of loops. Symbolic complexity bounds of loops, which are upper bounds of iteration times of loops, can be used to measure time complexity and prove termination of loops. Firstly, recurrence equations are generated to specify variables of loops and closed form solutions are computed. Secondly, an optimization problem is constructed which uses closed form solution and negative of loop condition as constraints, uses the variable specifies iteration times of loop as optimization object. Finally, the optimal solution of the optimization problem is the complexity bound. This approach can prove termination of programs without ranking functions and polynomial loop invariants. Compared with some other works, our approach can get more accurate complexity bounds of loops.4. Proving conditional termination of programs is the problem to find the preconditions for termination. We present a method of proving conditional termination based on polyranking and constraint solving. For phase-change programs, we can compute the preconditions needed. Compared with another work, our method works more efficiently.