Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Quantified Invariant Generation using Symbolic Computation and Theorem Proving

  • Speaker:   Dr  Laura Kovacs  (Ecole Polytechnique Federale de Lausanne (EPFL))
  • Host:   Andrei Voronkov
  • 1st April 2009 at 14:15 in Lecture Theatre 1.4, Kilburn Building
We address the problem of automatically inferring quantified invariants for programs over arrays, and present two novel approaches with different strengths. Both techniques require no user guidance.

The first approach being presented derives quantified invariants for programs iterating over multi-dimensional arrays. For instance, when used on matrices, our technique is able to infer their shape as a type invariant (upper-triangular, diagonal, etc). For doing so, we first transform a loop iterating over a multi-dimensional array into an equivalent sequence of unnested loops iterating over a one-dimensional array. Next, we infer quantified loop invariants for each unnested loop using a generalization of a recurrence-based invariant generation technique. The matrix type invariant is finally given by the conjunction of the quantified invariants of the unnested loops. We have implemented our approach in Aligator. When run on the Java matrix package JAMA, our technique is able to automatically infer all matrix shapes as type invariants that are guaranteed by JAMA's API. This is a joint work with Tom Henzinger and Thibaud Hottelier, EPFL.

The second approach uses symbolic computation and first order theorem proving, and allows one to generate quantified invariants with quantifier alternations for one-dimensional arrays. The method is based on the automatic analysis of the so-called update predicates of loops. An update predicate for an array expresses updates made to the array. 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. We run the theorem prover Vampire on some examples and show that non-trivial loop invariants can be generated. This is a joint work with Andrei Voronkov, University of Manchester.
▲ Up to the top