Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?

DOI10.1365/s13291-016-0138-1zbMath1372.65140OpenAlexW2429814779MaRDI QIDQ335016

Siegfried Michael Rump

Publication date: 2 November 2016

Published in: Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1365/s13291-016-0138-1

zbMATH Keywords

algorithminterval arithmeticfloating-point arithmetic

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Algorithms with automatic result verification (65G20) Numerical algorithms for computer arithmetic, etc. (65Y04)

Related Items (2)

Verified inclusions for a nearest matrix of specified rank deficiency via a generalization of Wedin's \(\sin (\theta)\) theorem ⋮ Mathematically rigorous global optimization in floating-point arithmetic

Uses Software

• ADOL-C
• Coq
• Maple
• Matlab
• ADIFOR
• MPFR
• INTLAB
• mctoolbox
• HOL Light
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The SIAM 100-Digit Challenge: a decade later. Inspirations, ramifications, and other eddies left in its wake
• A generalization of \(p\)-boxes to affine arithmetic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Error estimation of floating-point summation and dot product
• Error analysis of floating-point computation
• Inversion of extremely ill-conditioned matrices in floating-point
• Symmetry and related properties via the maximum principle
• Adaptive precision floating-point arithmetic and fast robust geometric predicates
• Multiple solutions for a semilinear boundary value problem: a computational multiplicity proof.
• Rump's example revisited
• A polyhedral branch-and-cut approach to global optimization
• Accurate solution of dense linear systems I: Algorithms in rounding to nearest
• Affine arithmetic: concepts and applications
• A floating-point technique for extending the available precision
• The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
• Improved Error Bounds for Inner Products in Floating-Point Arithmetic
• Verification methods: Rigorous results using floating-point arithmetic
• Improved Backward Error Bounds for LU and Cholesky Factorizations
• HOL Light: An Overview
• Average-Case Stability of Gaussian Elimination
• MPFR
• Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
• Rigorous Error Bounds for the Optimal Value in Semidefinite Programming
• Handbook of Floating-Point Arithmetic
• Iterative Refinement Implies Numerical Stability for Gaussian Elimination
• Gaussian Elimination with Partial Pivoting Can Fail in Practice
• On the Sensitivity of Solution Components in Linear Systems of Equations
• Algorithm 755: ADOL-C
• A mathematical view of automatic differentiation
• Large Growth Factors in Gaussian Elimination with Pivoting
• Accuracy and Stability of Numerical Algorithms
• The SIAM 100-Digit Challenge
• Rundungsfehleranalyse einiger Verfahren zur Summation endlicher Summen
• A Collection of Problems for Which Gaussian Elimination with Partial Pivoting is Unstable
• Theorem Proving in Higher Order Logics
• The Problem of Integration in Finite Terms
• Some Comments from a Numerical Analyst
• Modern Error Analysis
• Accurate Sum and Dot Product
• Numerical inverting of matrices of high order
• ROUNDING-OFF ERRORS IN MATRIX PROCESSES
• Some New Methods in Matrix Calculation
• Numerical linear algebra. A concise introduction with MATLAB and Julia
• A remarkable example of catastrophic cancellation unraveled

This page was built for publication: Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?