Towards Verified Rounding Error Analysis for Stationary Iterative Methods

Reference. Towards Verified Rounding Error Analysis for Stationary Iterative Methods

Ariel E. Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, Geoffrey Hulette · Correctness · 2022 · numerical-verification · DOI

Cite

Cite as @kellison-2022-towards (helia, typst) · \cite{kellison-2022-towards} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{kellison-2022-towards, title={Towards Verified Rounding Error Analysis for Stationary Iterative Methods}, url={http://dx.doi.org/10.1109/correctness56720.2022.00007}, DOI={10.1109/correctness56720.2022.00007}, booktitle={2022 IEEE/ACM Sixth International Workshop on Software Correctness for HPC Applications (Correctness)}, publisher={IEEE}, author={Kellison, Ariel and Tekriwal, Mohit and Jeannin, Jean-Baptiste and Hulette, Geoffrey}, year={2022}, month=Nov, pages={10–17} }

hayagriva YAML (typst)

yaml · 17 lines

kellison-2022-towards:
  type: article
  title: Towards Verified Rounding Error Analysis for Stationary Iterative Methods
  author:
  - Kellison, Ariel
  - Tekriwal, Mohit
  - Jeannin, Jean-Baptiste
  - Hulette, Geoffrey
  date: 2022-11
  page-range: 10-17
  url: http://dx.doi.org/10.1109/correctness56720.2022.00007
  serial-number:
    doi: 10.1109/correctness56720.2022.00007
  parent:
    type: proceedings
    title: 2022 IEEE/ACM Sixth International Workshop on Software Correctness for HPC Applications (Correctness)
    publisher: IEEE

Download: kellison-2022-towards.bib · kellison-2022-towards.yml

Cited by (1)

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method tekriwal-2023-verifiedCICM · 2023

DOI

Cites 47 works (1 here)

With notes (1)

Verified Software Toolchain appel_vst_2011ESOP · 2011

External (46)

Coq’s vibrant ecosystem for verification engineering (invited talk) (2022)
Verified Numerical Methods for Ordinary Differential Equations (2022)
Dandelion: Certified Approximations of Elementary Functions (2022)
Introduction and contents — Coq 8.15.2 documentation (2022)
VCFloat2: Floating-point Error Analysis in Coq (2022)
Formal verification of iterative convergence of numerical algorithms (2022)
A Perron–Frobenius theorem for deciding matrix growth (2021)
A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes (2021)
On the cost of iterative computations (2020)
QED at large: A survey of engineering of formally verified software (2020)
C-language floating-point proofs layered with VST and Flocq (2020)
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (2019)
A verified ode solver and smales 14th problem (2018)
The Flow of ODEs: Formalization of Variational Equation and Poincaré Map (2018)
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 (2018)
A formally verified floating-point implementation of the compact position reporting algorithm (2018)
Report of the HPC Correctness Summit, January 25-26, 2017, Washington, DC (2017)
The Flow of ODEs (2016)
A unified Coq framework for verifying C programs with floating-point computations (2016)
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
Compcert-a formally verified optimizing compiler (2016)
Applied Mathematics Research for Exascale Computing (2014)
Coquelicot: A User-Friendly Library of Real Analysis for Coq (2014)
Trusting computations: A mechanized proof from partial differential equations to actual program (2014)
Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations (2014)
Formalization of Matrix Theory in HOL4 (2014)
Certified, Efficient and Sharp Univariate Taylor Models in COQ (2013)
Matrices a blocs et en forme canonique (2013)
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program (2012)
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL (2012)
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL (2012)
Floating-point arithmetic in the Coq system (2012)
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq (2011)
Formal verification for numerical methods (2010)
Formal Proof of a Wave Equation Resolution Scheme: The Method Error (2010)
Packaging Mathematical Structures (2009)
Certified Exact Transcendental Real Number Computation in Coq (2008)
A Brief Overview of HOL4 (2008)
Floating-Point Verification Using Theorem Proving (2006)
Iterative Methods for Sparse Linear Systems (2003)
Accuracy and Stability of Numerical Algorithms (2002)
Floating point verification in HOL Light: The exponential function (2000)
HOL Light: A tutorial introduction (1996)
Defining the IEEE-854 floating-point standard in PVS (1995)
Componentwise Error Analysis for Stationary Iterative Methods (1993)
PVS: A prototype verification system (1992)