swMATH6800MaRDI QIDQ18875FDOQ18875
Author name not available (Why is that?)
Official website: http://flocq.gforge.inria.fr/
Cited In (48)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- FPTaylor
- CBench
- ValidSDP
- A Coq formalization of Lebesgue integration of nonnegative functions
- A validated real function calculus
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Deductive verification of floating-point Java programs in KeY
- Certified roundoff error bounds using semidefinite programming
- Primitive Floats in Coq
- A parameterized floating-point formalizaton in HOL Light
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Handbook of floating-point arithmetic
- Verified compilation of floating-point computations
- Computer Certified Efficient Exact Reals in Coq
- Axiomatic reals and certified efficient exact real computation
- Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Gappa
- core 2
- Ariadne
- C-CoRN
- iRRAM
- NLCertify
- Sollya
- Coquelicot
- CRlibm
- SoftFloat
- CAMPARY
- QD
- Proving tight bounds on univariate expressions with elementary functions in Coq
- FLIP
- CR-LIBM
- FloPoCo
- doubledouble
- DPE
- Algorithm 978
- Algorithm 539
- Coq Interval
- Computer-assisted verification of four interval arithmetic operators
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Stupid is as stupid does: taking the square root of the square of a floating-point number
- Formal verification of a floating-point expansion renormalization algorithm
- Computing a correct and tight rounding error bound using rounding-to-nearest
- HolPy
- Innocuous Double Rounding of Basic Arithmetic Operations
- A formal C memory model for separation logic
- Algorithm 1014
This page was built for software: Flocq
