Logo EPFL
I&C
Ecole Polytechnique Fédérale de Lausanne
Valigator Tool
english only

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:

Valigator was implemented in the Scala programming language. It

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

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.

Copyright © 2008 Thibaud Hottelier and Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.

Download

The tool is contained in and is accompanied by the demo file

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.