LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs

Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The LAProof library provides formal machine-checked proofs of the accuracy of basic linear algebra operations: inner product using conventional multiply and add, inner product using fused multiply-add, scaled matrix-vector and matrix-matrix multiplication, and scaled vector and matrix addition. These proofs can connect to concrete implementations of low-level basic linear algebra subprograms; as a proof of concept we present a machine-checked correctness proof of a C function implementing sparse matrix-vector multiplication using the compressed sparse row format. Our accuracy proofs are backward error bounds and mixed backward-forward error bounds that account for underflow, proved subject to no assumptions except a low-level formal model of IEEE-754 arithmetic. We treat low-order error terms concretely, not approximating as O(u2).

Original languageEnglish (US)
Title of host publicationProceedings - 2023 IEEE 30th Symposium on Computer Arithmetic, ARITH 2023
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages36-43
Number of pages8
ISBN (Electronic)9798350319224
DOIs
StatePublished - 2023
Externally publishedYes
Event30th IEEE Symposium on Computer Arithmetic, ARITH 2023 - Portland, United States
Duration: Sep 4 2023Sep 6 2023

Publication series

NameProceedings - Symposium on Computer Arithmetic

Conference

Conference30th IEEE Symposium on Computer Arithmetic, ARITH 2023
Country/TerritoryUnited States
CityPortland
Period9/4/239/6/23

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Keywords

  • floating-point arithmetic
  • formal verification
  • program verification
  • rounding error analysis

Fingerprint

Dive into the research topics of 'LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs'. Together they form a unique fingerprint.

Cite this