Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
From MaRDI portal
Publication:2013318
DOI10.1007/S10817-015-9339-ZzbMATH Open1409.68263OpenAlexW2138211565WikidataQ113901249 ScholiaQ113901249MaRDI QIDQ2013318FDOQ2013318
Authors: Pierre Roux 
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
Recommendations
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Floating-point arithmetic in the Coq system
- A parameterized floating-point formalizaton in HOL Light
- Certified roundoff error bounds using semidefinite programming
- Proving tight bounds on univariate expressions with elementary functions in Coq
Cholesky decompositionnumerical analysismatricesCoqproof assistantfloating-point arithmeticrounding error
Cites Work
- Verification methods: rigorous results using floating-point arithmetic
- Improved backward error bounds for LU and Cholesky factorizations
- Title not available (Why is that?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Canonical Big Operators
- Formal proof of a wave equation resolution scheme: the method error
- Verification of positive definiteness
- Construction of real algebraic numbers in Coq
- Title not available (Why is that?)
Cited In (6)
- Formally-verified round-off error analysis of Runge-Kutta methods
- Certification of bounds on expressions involving rounded operators
- Primitive Floats in Coq
- Enabling floating-point arithmetic in the Coq proof assistant
- Computer-assisted verification of four interval arithmetic operators
- Validating numerical semidefinite programming solvers for polynomial invariants
Uses Software
This page was built for publication: Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2013318)
