COO到CSR稀疏矩阵转换的形式化验证（特邀论文）
数值分析
2025-10-16 v1 计算机科学中的逻辑
数值分析
摘要
我们描述了一个将坐标格式（COO）稀疏矩阵转换为压缩稀疏行格式（CSR）矩阵的C程序的机器检查正确性证明。经典算法（按行、列的字典序对COO条目进行排序；从左到右填充CSR数组）虽然简洁，但具有相当复杂的不变量。我们阐述了一种从程序推导不变量的自底向上方法论。
引用
@article{arxiv.2510.13412,
title = {Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)},
author = {Andrew W. Appel},
journal= {arXiv preprint arXiv:2510.13412},
year = {2025}
}
备注
In 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