Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)

Abstract

We describe a machine-checked correctness proof of a C program that converts a coordinate-form (COO) sparse matrix to a compressed-sparse-row (CSR) matrix. The classic algorithm (sort the COO entries in lexicographic order by row,column; fill in the CSR arrays left to right) is concise but has rather intricate invariants. We illustrate a bottom-up methodology for deriving the invariants from the program.

arXiv commentIn Proceedings VSS 2025, arXiv:2510.12314. This paper accompanies my keynote lecture "Foundational end-to-end verification of numerical programs" at VSS 2025, the International Workshop on Verification of Scientific Software; and covers one of the results described in that talk