Pages that link to "Item:Q3541683"
From MaRDI portal
The following pages link to Proving Bounds on Real-Valued Functions with Computations (Q3541683):
Displaying 18 items.
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- Computing the range of values of real functions with accuracy higher than second order (Q761019) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Axiomatic reals and certified efficient exact real computation (Q2148797) (← links)
- Formalization of Bernstein polynomials and applications to global optimization (Q2351165) (← links)
- Affine Arithmetic and Applications to Real-Number Proving (Q2945641) (← links)
- Certification of bounds on expressions involving rounded operators (Q2989081) (← links)
- (Q3081652) (← links)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- Combining Coq and Gappa for Certifying Floating-Point Programs (Q3637269) (← links)
- (Q4989411) (← links)
- Multi-Prover Verification of Floating-Point Programs (Q5747756) (← links)
- A certificate-based approach to formally verified approximations (Q5875414) (← links)
- Formally-verified round-off error analysis of Runge-Kutta methods (Q6149594) (← links)
- Semantics, specification logic, and Hoare logic of exact real computation (Q6563064) (← links)
