Program Verification Based On Computer Algebra

In this thesis we consider how to verify the total correctness of a program from threedifferent aspects: invariant generation, invariant checking and termination analysis.For the invariant generation, first we prove that the invariants generated by Abstract In-terpretation are inductive invariants; then Mine's methods for generating invariants inZone and Octagon abstract domain are improved; finally the definition of the inductiveinvariants is extended, a new kind of invariants, inside-loop invariants, is obtained andwith this new definition invariants instead of the inductive invariants can be generated.For the invariant checking, a necessary and sufficient condition for an assertion beingan invariant at the location following loop constraints is presented. Since this theoremonly holds for a class of programs, for those programs not satisfying the requirementof this theorem another theorem for determining an assertion is not an invariant is de-veloped. With these methods a bug in the Fibonacci search in Wikipedia is detected.For the termination analysis we focus on the termination of linear programs with linearconstraints and polynomial constraints. For those with linear constraints Tiwari's workis improved; for those with polynomial constraints we prove that when program vari-ables are integers their termination is undecidable, and when the program variables arereals an algorithm for determining their termination is provided.