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