collaborators

1 paper

math.NA2025

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

Andrew W. Appel

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 (s…