Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions

DOI10.1007/978-3-319-19249-9_33zbMath1427.65064OpenAlexW2295915207MaRDI QIDQ5206960

Zvonimir Rakamarić, Ganesh Gopalakrishnan, Alexey Solovyev, Charles Jacobsen

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

zbMATH Keywords

global optimizationfloating-pointround-off error analysis

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Roundoff error (65G50)

Related Items (7)

Rigorous roundoff error analysis of probabilistic floating-point computations ⋮ A two-phase approach for conditional floating-point verification ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Counterexample- and simulation-guided floating-point loop invariant synthesis ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ Combining tools for optimization and analysis of floating-point computations ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Deciding floating-point logic with abstract conflict driven clause learning
• Floating-point arithmetic in the Coq system
• Semantics of roundoff error propagation in finite precision calculations
• Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY
• Taylor forms -- use and limits.
• Automatic detection of floating-point exceptions
• Certification of bounds on expressions involving rounded operators
• Static Analysis of Finite Precision Computations
• HOL Light: An Overview
• Interacting with Modal Logics in the Coq Proof Assistant
• GlobSol user guide
• ICOS: a branch and bound based solver for rigorous global optimization
• MPFR
• Software for Roundoff Analysis
• Automatic Error Analysis Using Computer Algebraic Manipulation
• Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
• Complete search in continuous global optimization and constraint satisfaction
• Programming Languages and Systems
• The MathSAT5 SMT Solver
• An Introduction to Affine Arithmetic
• Sound compilation of reals
• How do you compute the midpoint of an interval?
• Formal Methods for Hardware Verification

This page was built for publication: Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions