Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
From MaRDI portal
Publication:2013318
DOI10.1007/s10817-015-9339-zzbMath1409.68263OpenAlexW2138211565WikidataQ113901249 ScholiaQ113901249MaRDI QIDQ2013318
Publication date: 17 August 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9339-z
matricesfloating-point arithmeticnumerical analysisproof assistantCholesky decompositionCoqrounding error
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Computer-assisted verification of four interval arithmetic operators ⋮ Enabling floating-point arithmetic in the Coq proof assistant ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Primitive Floats in Coq ⋮ Validating numerical semidefinite programming solvers for polynomial invariants
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Verification of positive definiteness
- Verification methods: Rigorous results using floating-point arithmetic
- Construction of Real Algebraic Numbers in Coq
- Improved Backward Error Bounds for LU and Cholesky Factorizations
- Canonical Big Operators
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error
This page was built for publication: Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
