Formal verification of a floating-point expansion renormalization algorithm

DOI10.1007/978-3-319-66107-0_7zbMath1483.68479OpenAlexW2736053689MaRDI QIDQ1687723

Sylvie Boldo, Jean-Michel Muller, Mioara Joldes, Valentina Popescu

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_7

zbMATH Keywords

floating-point arithmeticformal proofCoqmultiple-precision arithmeticfloating-point expansions

Mathematics Subject Classification ID

Error analysis and interval analysis (65G99) Numerical algorithms for computer arithmetic, etc. (65Y04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Computational logic: its origins and applications ⋮ Computation of the unit in the first place (ufp) and the unit in the last place (ulp) in precision-\(p\) base \(\beta\) ⋮ Formally-verified round-off error analysis of Runge-Kutta methods

Uses Software

• Coq
• MPFR
• Flocq
• CAMPARY

Cites Work

• Adaptive precision floating-point arithmetic and fast robust geometric predicates
• High-precision arithmetic in mathematical physics
• CAMPARY: Cuda Multiple Precision Arithmetic Library and Applications
• Improved Error Bounds for Inner Products in Floating-Point Arithmetic
• Arithmetic Algorithms for Extended Precision Using Floating-Point Expansions
• MPFR
• Handbook of Floating-Point Arithmetic
• Accurate Floating-Point Summation Part I: Faithful Rounding
• On the Computation of Correctly Rounded Sums
• Accurate Sum and Dot Product