TY - GEN

T1 - Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver

T2 - Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023

AU - Tekriwal, Mohit

AU - Appel, Andrew W.

AU - Kellison, Ariel E.

AU - Bindel, David

AU - Jeannin, Jean Baptiste

N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2023

Y1 - 2023

N2 - Solving a sparse linear system of the form Ax= b is a common engineering task, e.g., as a step in approximating solutions of differential equations. Inverting a large matrix A is often too expensive, and instead engineers rely on iterative methods, which progressively approximate the solution x of the linear system in several iterations, where each iteration is a much less expensive (sparse) matrix-vector multiplication. We present a formal proof in the Coq proof assistant of the correctness, accuracy and convergence of one prominent iterative method, the Jacobi iteration. The accuracy and convergence properties of Jacobi iteration are well-studied, but most past analyses were performed in real arithmetic; instead, we study those properties, and prove our results, in floating-point arithmetic. We then show that our results are properly reflected in a concrete implementation in the C language. Finally, we show that the iteration will not overflow, under assumptions that we make explicit. Notably, our proofs are faithful to the details of the implementation, including C program semantics and floating-point arithmetic.

AB - Solving a sparse linear system of the form Ax= b is a common engineering task, e.g., as a step in approximating solutions of differential equations. Inverting a large matrix A is often too expensive, and instead engineers rely on iterative methods, which progressively approximate the solution x of the linear system in several iterations, where each iteration is a much less expensive (sparse) matrix-vector multiplication. We present a formal proof in the Coq proof assistant of the correctness, accuracy and convergence of one prominent iterative method, the Jacobi iteration. The accuracy and convergence properties of Jacobi iteration are well-studied, but most past analyses were performed in real arithmetic; instead, we study those properties, and prove our results, in floating-point arithmetic. We then show that our results are properly reflected in a concrete implementation in the C language. Finally, we show that the iteration will not overflow, under assumptions that we make explicit. Notably, our proofs are faithful to the details of the implementation, including C program semantics and floating-point arithmetic.

KW - Formal Verification

KW - Jacobi Method

KW - Numerical Methods

UR - http://www.scopus.com/inward/record.url?scp=85172127534&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85172127534&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-42753-4_14

DO - 10.1007/978-3-031-42753-4_14

M3 - Conference contribution

AN - SCOPUS:85172127534

SN - 9783031427527

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 206

EP - 221

BT - Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings

A2 - Dubois, Catherine

A2 - Kerber, Manfred

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 5 September 2023 through 8 September 2023

ER -