Certification of bounds on expressions involving rounded operators
From MaRDI portal
Publication:2989081
Recommendations
- Certified roundoff error bounds using semidefinite programming
- Bounds on the objective value of feasible roundings
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- A unified rounding error bound for polynomial evaluation
- Exact bounds for some basis functions of approximation operators
- Publication:4885353
- Proving Bounds on Real-Valued Functions with Computations
- scientific article; zbMATH DE number 5036728
- Bounds for an operator concave function
- Explicit bounds on certain integral inequalities
Cited in
(12)- Formally-verified round-off error analysis of Runge-Kutta methods
- An approximation framework for solvers and decision procedures
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Runtime abstract interpretation for numerical accuracy and robustness
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Gappa
- Formally verified roundoff errors using SMT-based certificates and subdivisions
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Computer-assisted verification of four interval arithmetic operators
- Rigorous roundoff error analysis of probabilistic floating-point computations
- Polynomial function intervals for floating-point software verification
- A Why3 proof of GMP algorithms
This page was built for publication: Certification of bounds on expressions involving rounded operators
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2989081)
