In this talk we describe how the combination of automated reasoning and symbolic
computation methods can be used to automatically generate statements expressing
arbitrarily complex computer program properties. The common method of the the talk
is our recently introduced symbol elimination method. The approach requires no
preliminary knowledge about program behavior, uses the power of a theorem prover
and/or symbolic computation algorithms, such as Groebner basis computation,
and infers quantified loop invariants and interpolants. We will also present recent
developments of symbol elimination in the Vampire theorem prover.