Verifying a Sparse Matrix Algorithm Using Symbolic Execution

TL;DR

The paper addresses verifying scientific software by applying symbolic execution to a CRS sparse matrix–dense vector multiply, using CIVL with a real-number model for floating point to treat verification as code-based specification. It demonstrates a driver-based workflow that non-deterministically generates valid CRS inputs, executes the algorithm, and checks functional equivalence against a dense reference via $mat\_vec\_mul$, within bounded input spaces. The approach yields strong verification guarantees within the chosen bounds and offers practical insights into debugging and expanding bounds, illustrating how symbolic execution complements traditional proofs. Overall, symbolic execution with CIVL provides a pragmatic, scalable path to early bug detection and verification in complex numerical code, while remaining compatible with later, more deductive verification techniques.

Abstract

Scientific software is, by its very nature, complex. It is mathematical and highly optimized which makes it prone to subtle bugs not as easily detected by traditional testing. We outline how symbolic execution can be used to write tests similar to traditional unit tests while providing stronger verification guarantees and apply this methodology to a sparse matrix algorithm.

Figures (5)

• Figure 1: sparse.h
• Figure 2: sparse.c : m and v are input parameters and p is an output
• Figure 3: matrix.cvh
• Figure 4: matrix.cvl
• Figure 5: driver.cvl