Software

Invariant and Type Inference for Matrices

Download Now Date Added: Oct 2009
Format: PDF

The authors present a loop property generation method for loops iterating over multi-dimensional arrays. When used on matrices, the authors' method is able to infer their shapes (also called types), such as upper-triangular, diagonal, etc. To generate loop properties, they first transform a nested loop iterating over a multidimensional array into an equivalent collection of unnested loops. Then, they infer quantified loop invariants for each unnested loop using a generalization of a recurrence-based invariant generation technique. These loop invariants give people conditions on matrices from which the authors can derive matrix types automatically using theorem provers.