Formal verification of a floating-point expansion renormalization algorithm
From MaRDI portal
Recommendations
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Floating-point arithmetic in the Coq system
- scientific article; zbMATH DE number 67109
- scientific article; zbMATH DE number 1614683
- Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
Cites work
- Accurate Floating-Point Summation Part I: Faithful Rounding
- Accurate Sum and Dot Product
- Adaptive precision floating-point arithmetic and fast robust geometric predicates
- Arithmetic Algorithms for Extended Precision Using Floating-Point Expansions
- CAMPARY: CUDA multiple precision arithmetic library and applications
- Handbook of Floating-Point Arithmetic
- High-precision arithmetic in mathematical physics
- Improved error bounds for inner products in floating-point arithmetic
- MPFR
- On the Computation of Correctly Rounded Sums
Cited in
(6)- A formally verified floating-point implementation of the compact position reporting algorithm
- Formally-verified round-off error analysis of Runge-Kutta methods
- Computation of the unit in the first place (ufp) and the unit in the last place (ulp) in precision-\(p\) base \(\beta\)
- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
- Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
- Computational logic: its origins and applications
This page was built for publication: Formal verification of a floating-point expansion renormalization algorithm
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687723)
