Invariant and Type Inference for Matrices

12 years 3 months ago
Invariant and Type Inference for Matrices
We present a loop property generation method for loops iterating over multi-dimensional arrays. When used on matrices, our method is able to infer their shapes (also called types), such as upper-triangular, diagonal, etc. To generate loop properties, we first transform a nested loop iterating over a multidimensional array into an equivalent collection of unnested loops. Then, we infer quantified loop invariants for each unnested loop using a generalization of a recurrence-based invariant generation technique. These loop invariants give us conditions on matrices from which we can derive matrix types automatically using theorem provers. Invariant generation is implemented in the software package Aligator and types are derived by theorem provers and SMT solvers, including Vampire and Z3. When run on the Java matrix package JAMA, our tool was able to infer automatically all matrix types describing the matrix shapes guaranteed by JAMA's API.
Thomas A. Henzinger, Thibaud Hottelier, Laura Kov&
Added 05 Mar 2010
Updated 08 Mar 2010
Type Conference
Year 2010
Authors Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov
Comments (0)