TY - GEN
T1 - Bounded Verification of Sparse Matrix Computations
AU - Dyer, Tristan
AU - Altuntas, Alper
AU - Baugh, John
N1 - Publisher Copyright:
© 2019 IEEE.
PY - 2019/11
Y1 - 2019/11
N2 - 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.
AB - 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.
KW - mechanical verification
KW - sparse matrix formats
KW - state-based formal methods
UR - https://www.scopus.com/pages/publications/85078872146
U2 - 10.1109/Correctness49594.2019.00010
DO - 10.1109/Correctness49594.2019.00010
M3 - Conference contribution
AN - SCOPUS:85078872146
T3 - Proceedings of Correctness 2019: 3rd International Workshop on Software Correctness for HPC Applications - Held in conjunction with SC 2019: The International Conference for High Performance Computing, Networking, Storage and Analysis
SP - 36
EP - 43
BT - Proceedings of Correctness 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 3rd IEEE/ACM International Workshop on Software Correctness for HPC Applications, Correctness 2019
Y2 - 18 November 2019
ER -