Valigator: A verification tool with bound and invariant generation. We describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gr”obner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.