Certification of bounds on expressions involving rounded operators
DOI10.1145/1644001.1644003zbMATH Open1364.68328OpenAlexW1999470254WikidataQ113310518 ScholiaQ113310518MaRDI QIDQ2989081FDOQ2989081
Authors: Marc Daumas, Guillaume Melquiond 
Publication date: 19 May 2017
Published in: ACM Transactions on Mathematical Software (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1644001.1644003
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
interval arithmeticCoqHOL Lightforward error analysisproof obligationproof systemPVSfloating pointdyadic fraction
General methods in interval analysis (65G40) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (11)
- Runtime abstract interpretation for numerical accuracy and robustness
- Formally-verified round-off error analysis of Runge-Kutta methods
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- A Why3 proof of GMP algorithms
- Polynomial function intervals for floating-point software verification
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Gappa
- Rigorous roundoff error analysis of probabilistic floating-point computations
- Computer-assisted verification of four interval arithmetic operators
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- An approximation framework for solvers and decision procedures
Uses Software
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)
