Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
From MaRDI portal
Publication:5206960
Recommendations
- Certified roundoff error bounds using semidefinite programming
- Rigorous roundoff error analysis of probabilistic floating-point computations
- A reduced product of absolute and relative error bounds for floating-point analysis
- Interval Enclosures of Upper Bounds of Roundoff Errors Using Semidefinite Programming
- A two-phase approach for conditional floating-point verification
Cites work
- scientific article; zbMATH DE number 1731783 (Why is no real title available?)
- scientific article; zbMATH DE number 1263371 (Why is no real title available?)
- scientific article; zbMATH DE number 3281219 (Why is no real title available?)
- An Introduction to Affine Arithmetic
- Automatic Error Analysis Using Computer Algebraic Manipulation
- Automatic detection of floating-point exceptions
- Certification of bounds on expressions involving rounded operators
- Complete search in continuous global optimization and constraint satisfaction
- Deciding floating-point logic with abstract conflict driven clause learning
- Floating-point arithmetic in the Coq system
- Formal Methods for Hardware Verification
- GlobSol user guide
- HOL Light: An Overview
- How do you compute the midpoint of an interval?
- ICOS: a branch and bound based solver for rigorous global optimization
- Interacting with Modal Logics in the Coq Proof Assistant
- MPFR
- Miller analyzer for Matlab: a Matlab package for automatic roundoff analysis
- Programming Languages and Systems
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Semantics of roundoff error propagation in finite precision calculations
- Software for Roundoff Analysis
- Sound compilation of reals
- Static analysis of finite precision computations
- Taylor forms -- use and limits.
- Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY
- The MathSAT5 SMT solver
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Cited in
(14)- Rigorous floating-point mixed-precision tuning
- A reduced product of absolute and relative error bounds for floating-point analysis
- Runtime abstract interpretation for numerical accuracy and robustness
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Certified roundoff error bounds using semidefinite programming
- Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Combining tools for optimization and analysis of floating-point computations
- Rigorous roundoff error analysis of probabilistic floating-point computations
- scientific article; zbMATH DE number 97115 (Why is no real title available?)
- Formally verified roundoff errors using SMT-based certificates and subdivisions
- Rigorous error analysis of numerical algorithms via symbolic computations
This page was built for publication: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5206960)
