Verified Optimization and Mapping of Sparse Tensor Algebra

Speaker: Scott Kovach, PhD Student, Stanford University
Date: April 6, 2022

Sparse tensor algebra is an important programming model in scientific and engineering domains that require high-confidence in accurate results. Automatic compilation methods can increase productivity and efficiency, but lack of trust in the compiler’s correctness may inhibit uptake. This talk will give an overview of methods in development for formally reasoning about compilers for sparse tensor algebra.

We will also discuss work in progress to mechanically verify a code-generator and hardware implementations for arbitrary tensor algebra using an interactive theorem prover. In addition to increasing trust, we also believe that the resulting system, where performance engineers can map applications to complex architectures with provable guarantees, will increase programmer productivity.