AIC Seminar Series
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover
Notice: Note the non-usual day (Wednesday) and time (3pm). Hosted by Richard Waldinger
Date: Wednesday September 09, 2009 at 15:00
Location: EJ228 (SRI E building) (Directions)
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).
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.
Please arrive at least 10 minutes early in order to sign in and be escorted to the conference room. SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the visitors lot in front of Building E, and should follow the instructions by the lobby phone to be escorted to the meeting room. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page.
©2013 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493