Thomas A. Henzinger, Thibaud Hottelier, and Laura Kovacs
We present Valigator, a software tool for imperative program verification which 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, Groebner basis computation, and quantifier elimination. We describe the general principles behind the implementation and illustrate them on examples.
Proceedings of the International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Lecture Notes in Computer Science 5330, Springer, 2008, pp. 333-342.