Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
From MaRDI portal
Publication:5206960
DOI10.1007/978-3-319-19249-9_33zbMATH Open1427.65064OpenAlexW2295915207MaRDI QIDQ5206960FDOQ5206960
Authors: Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamarić, Ganesh Gopalakrishnan 
Publication date: 19 December 2019
Published in: FM 2015: Formal Methods (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-19249-9_33
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
- Certification of bounds on expressions involving rounded operators
- ICOS: a branch and bound based solver for rigorous global optimization
- Programming Languages and Systems
- The MathSAT5 SMT solver
- Miller analyzer for Matlab: a Matlab package for automatic roundoff analysis
- Title not available (Why is that?)
- MPFR
- Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY
- HOL Light: An Overview
- Deciding floating-point logic with abstract conflict driven clause learning
- Complete search in continuous global optimization and constraint satisfaction
- GlobSol user guide
- Floating-point arithmetic in the Coq system
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Taylor forms -- use and limits.
- Static analysis of finite precision computations
- How do you compute the midpoint of an interval?
- Formal Methods for Hardware Verification
- An Introduction to Affine Arithmetic
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Interacting with Modal Logics in the Coq Proof Assistant
- Sound compilation of reals
- Semantics of roundoff error propagation in finite precision calculations
- Software for Roundoff Analysis
- Automatic Error Analysis Using Computer Algebraic Manipulation
- Automatic detection of floating-point exceptions
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (14)
- 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
- Title not available (Why is that?)
- Formally verified roundoff errors using SMT-based certificates and subdivisions
- Rigorous floating-point mixed-precision tuning
- Rigorous error analysis of numerical algorithms via symbolic computations
- A reduced product of absolute and relative error bounds for floating-point analysis
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)
