AIC Seminar Series

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
SRI International is an independent, nonprofit corporation. Privacy policy