Flocq
From MaRDI portal
Software:18875
No author found.
Related Items (23)
Axiomatic reals and certified efficient exact real computation ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Computer-assisted verification of four interval arithmetic operators ⋮ Handbook of Floating-Point Arithmetic ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case ⋮ Formal verification of a floating-point expansion renormalization algorithm ⋮ A formal C memory model for separation logic ⋮ A validated real function calculus ⋮ Primitive Floats in Coq ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Formal proofs of rounding error bounds. With application to an automatic positive definiteness check ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ 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 ⋮ Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest ⋮ Type classes for efficient exact real arithmetic in Coq ⋮ Innocuous Double Rounding of Basic Arithmetic Operations ⋮ Certified Roundoff Error Bounds Using Semidefinite Programming ⋮ Verified compilation of floating-point computations
This page was built for software: Flocq
