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

Reference. 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 · CICM · 2023 · numerical-verification · DOI

Cite

Cite as @tekriwal-2023-verified (helia, typst) · \cite{tekriwal-2023-verified} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{tekriwal-2023-verified, title={Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method}, ISBN={9783031427534}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-031-42753-4_14}, DOI={10.1007/978-3-031-42753-4_14}, booktitle={Intelligent Computer Mathematics}, publisher={Springer Nature Switzerland}, author={Tekriwal, Mohit and Appel, Andrew W. and Kellison, Ariel E. and Bindel, David and Jeannin, Jean-Baptiste}, year={2023}, pages={206–221} }

hayagriva YAML (typst)

yaml · 20 lines

tekriwal-2023-verified:
  type: chapter
  title: 'Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method'
  author:
  - Tekriwal, Mohit
  - Appel, Andrew W.
  - Kellison, Ariel E.
  - Bindel, David
  - Jeannin, Jean-Baptiste
  date: 2023
  page-range: 206-221
  url: http://dx.doi.org/10.1007/978-3-031-42753-4_14
  serial-number:
    doi: 10.1007/978-3-031-42753-4_14
    isbn: '9783031427534'
    issn: 1611-3349
  parent:
    type: book
    title: Intelligent Computer Mathematics
    publisher: Springer Nature Switzerland

Download: tekriwal-2023-verified.bib · tekriwal-2023-verified.yml

Cited by (1)

Formalization of Asymptotic Convergence for Stationary Iterative Methods tekriwal-2024-formalizationNFM · 2024

DOI

Cites 29 works (1 here)

With notes (1)

Towards Verified Rounding Error Analysis for Stationary Iterative Methods kellison-2022-towardsCorrectness · 2022

DOI

External (28)

LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs (2023)
Verified Numerical Methods for Ordinary Differential Equations (2022)
Formalization of Asymptotic Convergence for Stationary Iterative Methods (2022)
VCFloat2: Floating-point error analysis in Coq (2022)
A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes (2021)
A Perron–Frobenius theorem for deciding matrix growth (2021)
C-language floating-point proofs layered with VST and Flocq (2020)
The Flow of ODEs: Formalization of Variational Equation and Poincaré Map (2019)
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs (2018)
A Verified ODE Solver and Smale's 14th Problem (2018)
Coquelicot: A User-Friendly Library of Real Analysis for Coq (2015)
PageRank Beyond the Web (2015)
Trusting computations: A mechanized proof from partial differential equations to actual program (2014)
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program (2013)
Certified, Efficient and Sharp Univariate Taylor Models in COQ (2013)
Matrices à blocs et en forme canonique (2013)
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL (2012)
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq (2011)
Formal Verification for Numerical Methods (2010)
Packaging Mathematical Structures (2009)
Certified Exact Transcendental Real Number Computation in Coq (2008)
Iterative Methods for Sparse Linear Systems (2003)
Accuracy and Stability of Numerical Algorithms (2002)
Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods (1994)
Componentwise Error Analysis for Stationary Iterative Methods (1993)
Convergence Properties of the Spline Fit (1963)
Matrices with dominant diagonals and economic theory (1960)
A New Status Index Derived from Sociometric Analysis (1953)