Presentation
Bounded Verification of Sparse Matrix Computations
Event Type
Workshop
W
Algorithms
Correctness
Debugging
Reliability
Verification
TimeMonday, 18 November 20194:30pm - 5pm
Location712
DescriptionWe 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.
Archive