Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Andrew W. Appel

TL;DR

The paper addresses reliably converting a COO sparse matrix to CSR in C with a formal, machine-checked proof of correctness. It employs a bottom-up invariant-driven verification approach using the Verifiable Software Toolchain (VST) and Coq, separating data-structure reasoning from floating-point approximation. A complete semantic specification relates COO and CSR representations via $coo\_to\_matrix$ and $csr\_to\_matrix$, and provides a function spec for $coo\_to\_csr\_matrix$ bound by a floating-point sum relation that permits arbitrary summation order of duplicates. The authors report substantial formal effort (1571 lines of Coq, 412 lines of VST) and discuss issues of bit-for-bit reproducibility, reassembly, and future work on incremental updates, highlighting the practical impact of verified numerical software components.

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.

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

TL;DR

The paper addresses reliably converting a COO sparse matrix to CSR in C with a formal, machine-checked proof of correctness. It employs a bottom-up invariant-driven verification approach using the Verifiable Software Toolchain (VST) and Coq, separating data-structure reasoning from floating-point approximation. A complete semantic specification relates COO and CSR representations via and , and provides a function spec for bound by a floating-point sum relation that permits arbitrary summation order of duplicates. The authors report substantial formal effort (1571 lines of Coq, 412 lines of VST) and discuss issues of bit-for-bit reproducibility, reassembly, and future work on incremental updates, highlighting the practical impact of verified numerical software components.

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.
Paper Structure (2 sections, 1 equation, 3 figures)

This paper contains 2 sections, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. The specification

Figures (3)

  • Figure \thelstlisting: An example of the three arrays (, , ) used to store a matrix compressed sparse row (CSR) format. From Barret et al.barret94:templates, adjusted for 0-based array indexing.
  • Figure \thelstlisting: A coordinate-form representation of the matrix from \ref{['fig:CSR']}
  • Figure \thelstlisting: Mesh arising from an irregular finite-element problem. From https://en.wikipedia.org/wiki/Mesh_generation