Invariant and type inference for matrices

Henzinger TA, Hottelier T, Kovács L, Voronkov A. 2010. Invariant and type inference for matrices. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 163–179.

Download
OA IST-2012-69-v1+1_Invariant_and_type_inference_for_matrices.pdf 251.26 KB [Submitted Version]

Conference Paper | Published | English

Scopus indexed
Author
Henzinger, Thomas AISTA ; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei
Series Title
LNCS
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.
Publishing Year
Date Published
2010-01-01
Acknowledgement
The research was supported by the Swiss NSF.
Volume
5944
Page
163 - 179
Conference
VMCAI: Verification, Model Checking and Abstract Interpretation
Conference Location
Madrid, Spain
Conference Date
2010-01-17 – 2010-01-19
IST-REx-ID

Cite this

Henzinger TA, Hottelier T, Kovács L, Voronkov A. Invariant and type inference for matrices. In: Vol 5944. Springer; 2010:163-179. doi:10.1007/978-3-642-11319-2_14
Henzinger, T. A., Hottelier, T., Kovács, L., & Voronkov, A. (2010). Invariant and type inference for matrices (Vol. 5944, pp. 163–179). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-642-11319-2_14
Henzinger, Thomas A, Thibaud Hottelier, Laura Kovács, and Andrei Voronkov. “Invariant and Type Inference for Matrices,” 5944:163–79. Springer, 2010. https://doi.org/10.1007/978-3-642-11319-2_14.
T. A. Henzinger, T. Hottelier, L. Kovács, and A. Voronkov, “Invariant and type inference for matrices,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Madrid, Spain, 2010, vol. 5944, pp. 163–179.
Henzinger TA, Hottelier T, Kovács L, Voronkov A. 2010. Invariant and type inference for matrices. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 5944, 163–179.
Henzinger, Thomas A., et al. Invariant and Type Inference for Matrices. Vol. 5944, Springer, 2010, pp. 163–79, doi:10.1007/978-3-642-11319-2_14.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
Access Level
OA Open Access
Date Uploaded
2018-12-12
MD5 Checksum
da69b13a2d9a7a316c909e09c1090cef


Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar