2019 conference paper
Bounded Verification of Sparse Matrix Computations
2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 36–43.
author keywords: sparse matrix formats; state-based formal methods; mechanical verification
TL;DR:
To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates, relying on a formalism called Alloy to show that one model is a refinement of another.
(via Semantic Scholar)
UN Sustainable Development Goal Categories
11. Sustainable Cities and Communities
(Web of Science)
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.