Flocq

swMATH6800MaRDI QIDQ18875FDOQ18875

Author name not available (Why is that?)

Cited In (23)

• 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
• Primitive Floats in Coq
• A parameterized floating-point formalizaton in HOL Light
• Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest
• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
• 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
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Certified Roundoff Error Bounds Using Semidefinite Programming
• Type classes for efficient exact real arithmetic in Coq
• 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
• Innocuous Double Rounding of Basic Arithmetic Operations
• Handbook of Floating-Point Arithmetic
• A formal C memory model for separation logic

This page was built for software: Flocq