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.

Kurzbiography

Laura Kovács is a postdoctoral researcher in the Models and Theory of Computation research group of Prof. Dr. Thomas A. Henzinger at Ecole Polytechnique Federale de Lausanne, 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.

Hinweis

Beginn des Vortrags 16:00 Uhr s.t., Kaffee ab 15:30 Uhr

Speakers

• Laura Kovacs, Professor for Automated Reasoning, TU Wien

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!