Formal proofs of rounding error bounds. With application to an automatic positive definiteness check

DOI10.1007/S10817-015-9339-ZMaRDI QIDQ2013318zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

Cholesky decompositionnumerical analysismatricesCoqproof assistantfloating-point arithmeticrounding error

Mathematics Subject Classification ID

Roundoff error (65G50)

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

Cites work

• scientific article; zbMATH DE number 2185690 (Why is no real title available?)
• scientific article; zbMATH DE number 846277 (Why is no real title available?)
• Canonical Big Operators
• Construction of real algebraic numbers in Coq
• Formal proof of a wave equation resolution scheme: the method error
• Improved backward error bounds for LU and Cholesky factorizations
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Verification methods: rigorous results using floating-point arithmetic
• Verification of positive definiteness

Cited in

(10)

• Certified roundoff error bounds using semidefinite programming
• Formally-verified round-off error analysis of Runge-Kutta methods
• Formally verified certificate checkers for hardest-to-round computation
• Primitive Floats in Coq
• Certification of bounds on expressions involving rounded operators
• Computing a correct and tight rounding error bound using rounding-to-nearest
• Enabling floating-point arithmetic in the Coq proof assistant
• Formally verified roundoff errors using SMT-based certificates and subdivisions
• Validating numerical semidefinite programming solvers for polynomial invariants
• Computer-assisted verification of four interval arithmetic operators

Describes a project that uses

Uses Software

• Coq
• mctoolbox
• Flocq

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)