Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method

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

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

1 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationIntelligent Computer Mathematics - 16th International Conference, CICM 2023, Proceedings
EditorsCatherine Dubois, Manfred Kerber
PublisherSpringer Science and Business Media Deutschland GmbH
Pages206-221
Number of pages16
ISBN (Print)9783031427527
DOIs
StatePublished - 2023
EventProceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023 - Cambridge, United Kingdom
Duration: Sep 5 2023Sep 8 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14101 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceProceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023
Country/TerritoryUnited Kingdom
CityCambridge
Period9/5/239/8/23

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Keywords

  • Formal Verification
  • Jacobi Method
  • Numerical Methods

Fingerprint

Dive into the research topics of 'Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method'. Together they form a unique fingerprint.

Cite this