Solving in Theorema ∗ Presented at 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC04),

Abstract. Most of the properties established during program verification are either invariants or depend crucially on invariants. The effectiveness of auto-mated verification of (imperative) programs is therefore sensitive to the ease with which invariants, even trivial ones, can be automatically deduced. We present a method for invariant generation that relies on combinatorial tech-niques, namely on recurrence solving and variable elimination. We implemented the method within the mathematical assistant Theorema (www.theorema.org) and we demonstrate its effectiveness on several examples. Key words: program analysis and verification, invariant generation, symboli