---
res:
  bibo_abstract:
  - 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 gen- erate loop properties,
    we first transform a nested loop iterating over a multi- dimensional array into
    an equivalent collection of unnested loops. Then, we in- fer 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 us- ing 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Thibaud
      foaf_name: Hottelier, Thibaud
      foaf_surname: Hottelier
  - foaf_Person:
      foaf_givenName: Laura
      foaf_name: Kovács, Laura
      foaf_surname: Kovács
  - foaf_Person:
      foaf_givenName: Andrei
      foaf_name: Voronkov, Andrei
      foaf_surname: Voronkov
  bibo_doi: 10.1007/978-3-642-11319-2_14
  bibo_volume: 5944
  dct_date: 2010^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Invariant and type inference for matrices@
...