Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Laura KovácsETH Zurich[Home Page]

Notice:  Note the non-usual day (Wednesday) and time (3pm). Hosted by Richard Waldinger

Date:  2009-09-09 at 15:00

Location:  EJ228 (SRI E building)  (Directions)

   Abstract

Quantified loop invariants of programs over arrays can be automatically inferred using a first-order theorem prover, reducing the burden of annotating loops with complete invariants. Unlike other state-of-the-art methods, our approach allows one to generate first-order invariants containing alternations of quantifiers. For doing so, we deploy symbolic computation methods to generate numeric invariants of the scalar loop variables, based on the software package Aligator, and then use update predicates of the loop. An update predicate for an array A expresses updates made to A. We observe that many properties of update predicates can be extracted automatically from the loop description and loop properties obtained by other methods, such as a simple analysis of counters occurring in the loop, recurrence solving, and quantifier elimination over loop variables. The first-order information extracted from the loop description can use auxiliary symbols, such as symbols denoting update predicates or loop counters. After having collected the first-order information, we run the saturation theorem prover Vampire to eliminate the auxiliary symbols and obtain loop invariants expressed as first-order formulas. When the invariants obtained in this way contain skolem functions, we de-skolemise them into formulas with quantifier alternations. Our method does not require the user to give a post-condition, a predefined collection of predicates or any other form of human guidance and avoids inductive reasoning. Our experimental results on benchmark examples demonstrate the potential of our method. This is a joint work with Andrei Voronkov (University of Manchester, UK).

   Bio for Laura Kovács

Laura Kovács is a postdoctoral researcher in the Programming Methodology research group of Prof. Peter Mueller at ETH Zuerich, 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. Before joining ETH Zurich, she was a postdoctoral researcher at EPFL, Switzerland, in the Models and Theory of Computation research group of Prof. Thomas A. Henzinger.

   Note for Visitors to SRI

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E. SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking lots off Fourth Street. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. There are two entrances to SRI International located on Ravenswood Ave. Please check the Builing E entrance signage.

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy