SC19 Proceedings

The International Conference for High Performance Computing, Networking, Storage, and Analysis

Bounded Verification of Sparse Matrix Computations


Workshop: Bounded Verification of Sparse Matrix Computations

Abstract: 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.






Back to 3nd International Workshop on Software Correctness for HPC Applications (Correctness 2019) Archive Listing


Back to Full Workshop Archive Listing