Institute of Computer Languages
Compilers and Languages Group

Talks 2008 - Laura Kovacs

The Compilers and Languages Group invites you to a talk given by

Dr. Laura Kovacs

Ecole Polytechnique Federale de Lausanne, Switzerland

on

Invariant Generation by Algebraic Techniques for Software Verification

Date: Friday, November 28th, 2008
Time: 16:00 (s.t.)
Location: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)

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.

About Dr. Laura Kovacs:

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.

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)