Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method

DOI10.1007/978-3-031-42753-4_14OpenAlexW4386297788MaRDI QIDQ6118833

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

Publication date: 28 February 2024

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-42753-4_14

zbMATH Keywords

formal verificationJacobi methodNumerical methods

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• VST-Floyd: a separation logic tool to verify correctness of C programs
• The flow of ODEs: formalization of variational equation and Poincaré map
• Coquelicot: a user-friendly library of real analysis for Coq
• A Perron-Frobenius theorem for deciding matrix growth
• Trusting computations: a mechanized proof from partial differential equations to actual program
• A new status index derived from sociometric analysis
• PageRank Beyond the Web
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Packaging Mathematical Structures
• Certified Exact Transcendental Real Number Computation in Coq
• Accuracy and Stability of Numerical Algorithms
• C-language floating-point proofs layered with VST and Flocq
• Convergence Properties of the Spline Fit

This page was built for publication: Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method