Invariant Generation by Algebraic Techniques for Software Verification
Zusammenfassung
| Was | Invariant Generation by Algebraic Techniques for Software Verification |
|---|---|
| Wer | Dr. Laura KOVACS, Ecole Polytechnique Federale de Lausanne, Switzerland |
| Wo | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock |
| Wann |
28/11/08
16:00 |
| Link | http://mtc.epfl.ch/~likovacs/ |
Details
Abstract
We present a method for generating loop invariants and bound assertion for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses symbolic summation, Groebner basis computation, and quantifier elimination. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived.These techniques are implemented in a new software package Aligator, and successfully tried on many programs implementing interesting algorithms working on numbers. Moreover, we integrated Aligator in our new software tool for imperative program verification, named Valigator, that offers support for automatically generating and proving verification conditions in a uniform framework.