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.

翻译：本文描述了一个C程序的机器检验正确性证明，该程序将坐标格式（COO）稀疏矩阵转换为压缩稀疏行（CSR）矩阵。经典算法（按行、列字典序对COO条目排序；从左到右填充CSR数组）虽然简洁，但其不变量相当复杂。我们展示了一种自底向上从程序推导不变量的方法。