A generic library for floating-point numbers and its application to exact computing
From MaRDI portal
Recommendations
- An accurate elementary mathematical library for the IEEE floating point standard
- A library of parameterized floating-point modules and their use
- Accurate and efficient algorithms for floating point computation
- Arithmetic Algorithms for Extended Precision Using Floating-Point Expansions
- Faithfully rounded floating-point computations
- Accurate and reliable computing in floating-point arithmetic
- FloatX
- Numerical investigation of floating-point arithmetic
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
Cited in
(27)- Additive symmetries: The non-negative case.
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- A validated real function calculus
- Computing predecessor and successor in rounding to nearest
- Trusting computations: a mechanized proof from partial differential equations to actual program
- A parameterized floating-point formalizaton in HOL Light
- Motivations for an arbitrary precision interval arithmetic and the MPFI library
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Proving Bounds on Real-Valued Functions with Computations
- Combining Coq and Gappa for Certifying Floating-Point Programs
- An accurate elementary mathematical library for the IEEE floating point standard
- Deciding floating-point logic with abstract conflict driven clause learning
- FloatX
- Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
- Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
- Floating-Point LLL: Theoretical and Practical Aspects
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Multi-prover verification of floating-point programs
- The Design of Core 2: A Library for Exact Numeric Computation in Geometry and Algebra
- Floating-point arithmetic
- Finding normal binary floating-point factors efficiently
- Automatic Generation of Guard-Stable Floating-Point Code
- Provably correct floating-point implementation of a point-in-polygon algorithm
- Floating-point arithmetic in the Coq system
- Formal verification of the VAMP floating point unit
- Formalization of fixed-point arithmetic in HOL
- Semantics of roundoff error propagation in finite precision calculations
This page was built for publication: A generic library for floating-point numbers and its application to exact computing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4790659)
