Using Symbolic Summation and Polynomial Algebra for Imperative Program Verification in Theorema 1

An approach utilizing combinatorics, algebraic methods and logic is presented for generating polynomial loop invariants for a family of imperative programs operating on numbers. The approach has been implemented in the Theorema system, which seems ideal for such an integration given that it is built on top of the computer algebra system Mathematica, has a theorem prover for first-order logic as well as for mechanizing induction. These invariant assertions are then used for generating the necessary verification conditions as first-order logical formulae, based on Hoare logic and the weakest precondition strategy. The approach has been successfully tried on many programs implementing interesting number theoretic algorithms. It is also shown that for a subfamily of loops, called P-solvable loops, the approach is complete in generating polynomial equations as invariants.