The VALIGATOR Tool

Short Description

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:

they contain only assignments to variables and nested conditionals;
variables in assignments range over numeric types, such as e.g. integers;
variables can be expressed as a polynomial of the initial values of variables, the loop counter, and some new variables, where there are algebraic dependencies among the new variables;
assignments to variables from the loop condition are affine mappings (whose matrix equation yields only 1 as eigenvalues);
conditional branches in loops are commuting (variables from the loop tests are changed in the same manner on each branch);
loop condition is expressed by linear inequalities over loop variables.

Valigator was implemented in the Scala programming language. It

contains a prototype verification condition generator based on the strongest postcondition;
integrates Aligator as its invariant inference engine together with bound analysis of P-solvable loops;
uses the automated theorem provers Z3, CVC3 and STP for proving correctness of the verification conditions.

A Note on the Implementation

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

a 32 bit version of Java release 1.5 or higher;
a Scala version 2.6.0;
Mathematica 5.2 together with version 0.5 of Aligator;
the theorem provers Z3, CVC3 and STP.

Registration and Legal Notices

The source code is password protected. To get the password send an email to Thibaud Hottelier or Laura Kovács. It will be given for free to all researchers and non-commercial users.

Download

The tool is contained in

Valigator.tar.gz

and is accompanied by the demo file

Examples.pdf.

Literature

To use the implementation it is sufficient to study the demo files above. It contains many examples to start with.

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]

Versions and Bugs

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.