@inproceedings{251b1272bdaf4d2a80b9a5416fe003b9,

title = "LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs",

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).",

keywords = "floating-point arithmetic, formal verification, program verification, rounding error analysis",

author = "Kellison, {Ariel E.} and Appel, {Andrew W.} and Mohit Tekriwal and David Bindel",

note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 30th IEEE Symposium on Computer Arithmetic, ARITH 2023 ; Conference date: 04-09-2023 Through 06-09-2023",

year = "2023",

doi = "10.1109/ARITH58626.2023.00021",

language = "English (US)",

series = "Proceedings - Symposium on Computer Arithmetic",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "36--43",

booktitle = "Proceedings - 2023 IEEE 30th Symposium on Computer Arithmetic, ARITH 2023",

address = "United States",

}