Valigator is a software tool for imperative program verification that efficiently combines symbolic computation with computational logic in a uniform framework.
Valigator offers support for automatically generating and proving verification conditions, and most importantly automatically inferring loop invariants and bound assertions by means of symbolic summation, Groebner basis computation and quantifier elimination.
Inputs to Valigator are programs formulated in a custom language similar to a subset of the programming language C, with sequencing, assignments, conditionals and loops, involving addition and multiplication over numbers (integers). Data types are not yet handled.
We require that loops are P-solvable. Namely:
Valigator was implemented in the Scala programming language. It
Valigator was implemented in the Scala programming language, and integrates Scala with Mathematica in a completely transparent way. Using and controlling the Mathematica kernel directly from a Scala program is thus supported in Valigator.
To build Valigator, one needs
Copyright © 2008 Thibaud Hottelier and Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.
Further information can be found here:
T. A. Henzinger, T. Hottelier and L. Kovács (2008), Valigator: A Verification Tool with Bound and Invariant Generation. Proc. of LPAR 2008, LNCS 5330, pp. 333-342. [pdf]
The tool was written and developed at at MTC, EPFL, Switzerland.
Right now you are using Version 0.2, last updated on October 13, 2008.
Please report any bugs and comments to Thibaud Hottelier or Laura Kovács.