Institute of Computer Languages
Compilers and Languages Group
on
| Date: | Friday, November 28th, 2008 |
|---|---|
| Time: | 16:00 (s.t.) |
| Location: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |
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.
Laura Kovacs is a postdoctoral researcher in the Models and Theory of Computation research group of Prof. Dr. Thomas A. Henzinger at cole Polytechnique Federale 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. ( http://mtc.epfl.ch/~likovacs )
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.