Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
type: Item
instance of: scholarly article
title: Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
zbMATH Open document ID: 1409.68263
author: Pierre Roux
published in: Journal of Automated Reasoning
publication date: 2017-08-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 65G50
zbMATH DE Number: 6761449
zbMATH Keywords: floating-point arithmetic
zbMATH Keywords: rounding error
zbMATH Keywords: numerical analysis
zbMATH Keywords: proof assistant
zbMATH Keywords: Coq
zbMATH Keywords: matrices
zbMATH Keywords: Cholesky decomposition
describes a project that uses: Coq
describes a project that uses: Flocq
describes a project that uses: mctoolbox
MaRDI profile type: Publication
full work available at URL: s10817-015-9339-z
OpenAlex ID: W2138211565
Wikidata QID: Q113901249
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Canonical Big Operators
cites work: Formal Proof of a Wave Equation Resolution Scheme: The Method Error
cites work: Construction of Real Algebraic Numbers in Coq
cites work: Q3024872
cites work: Q4864704
cites work: Verification methods: rigorous results using floating-point arithmetic
cites work: Verification of positive definiteness
cites work: Improved backward error bounds for LU and Cholesky factorizations
DOI: 10.1007/S10817-015-9339-Z
description: scientific article; zbMATH DE number 6761449