Study On Program Verification Based On Symbolic Computation

Program verification is one of the frontier research topics in program design field, which has important theoretical significance and application value. In this dissertation, we introduce some classical algorithms in symbolic computation into program verification, and mainly do researches on program verification in three basic aspects:generation of program invariants, termination analysis and generation of preconditions.Loop invariants play a very important role in proving partial correctness of pro-grams. we mainly study the invariant generation of polynomial loop programs. We firstly present a new method for generating polynomial invariants of polynomial loop programs by computing vanishing ideal of sampling points. A reliable polynomial time algorithm for generating polynomial invariants is established.Termination analysis of loop programs is very important in many applications, es-pecially in those of safety critical software. In this dissertation, we mainly study the ter-mination of programs with polynomial guards and linear assignments. The discussion is based on simplifying the linear loops by its Jordan form. And then the process to find the nonterminating points for general polynomial guards be reduced to semi-algebraic system (SAS for short) solving. If the number of functions in SAS are finite or the functions are integer periodic, then the termination of programs is decidable.However, instead of considering complete termination of programs, i.e., termination for all inputs, we are more concerned with the following questions:How if the code only terminates for some inputs? In this dissertation, a rapid and reliable algorithm for gener-ating preconditions of loop programs with linear or nonlinear assignments is established. Clearly, a loop program can be elegantly expressed by means of a system of difference equations, which describes the behavior of the loop variables changing at each iteration. The method is based on solving systems of difference equations corresponding to the loop assignments, and then substituting the solutions into the loop guards to compute precon-ditions that ensure the termination of the loop programs.The results indicate that symbolic computation is a valid tool for studying program verification. We hope that more and more classical algorithms in symbolic computation can be introduced into research on program verification.