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.

Kurzbiographie von Dr. Laura KOVACS:

Laura Kovács is a postdoctoral researcher in the Models and Theory of
Computation research group of Prof. Dr. Thomas A. Henzinger at École Polytechnique Fédérale de Lausanne (EPFL), Switzerland.  Her research deals
with the design and development of new theories, technologies, and
tools for program verification, with a particular focus on automated
assertion generation, symbolic summation, computer algebra, and
automated theorem proving.  She holds an MSc from the Western
University of Timisoara, Romania, and a PhD degree from the Research
Institute for Symbolic Computation of the Johannes Kepler University,
Linz, Austria. ( <link service.zid.tuwien.ac.at/ts/goto.php _blank>http://mtc.epfl.ch/~likovacs/</link> )