Valigator: A Verification Tool with Bound and Invariant Generation

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.

Download inofficial, sometimes updated PDF document. © 2008 Springer.