2019 conference paper

Bounded Verification of Sparse Matrix Computations

2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 36–43.

By: T. Dyer n, A. Altuntas* & J. Baugh n

author keywords: sparse matrix formats; state-based formal methods; mechanical verification
Source: ORCID
Added: March 30, 2020

We show how to model and reason about the structure and behavior of sparse matrices, which are central to many applications in scientific computation. Our approach is state-based, relying on a formalism called Alloy to show that one model is a refinement of another. We present examples of sparse matrix-vector multiplication, transpose, and translation between formats using ELLPACK and compressed sparse row formats to demonstrate the approach. To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates. Mechanical verification is performed using SAT solvers built into the tool.