Verification Environment in Theorema

We present a verification environment for imperative programs (using Hoare logic) and for func- tional programs (using fixpoint theory) in the frame of the Theorema system (www.theorema.org). In particular, we discuss some methods for finding the invariants of loops and specifications of auxiliary tail recursive functions. These methods use techniques from (polynomial) algebra and combinatorics, namely Groebner bases, variable elim- ination and symbolic summation (the Gosper algorithm, the technique of generating functions). The methods are demonstrated on several examples which have been treated automatically by our implementation.