Certification of bounds on expressions involving rounded operators
From MaRDI portal
Publication:2989081
DOI10.1145/1644001.1644003zbMath1364.68328OpenAlexW1999470254WikidataQ113310518 ScholiaQ113310518MaRDI QIDQ2989081
Guillaume Melquiond, Marc Daumas
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
interval arithmeticproof systemforward error analysisCoqHOL Lightproof obligationPVSfloating pointdyadic fraction
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (11)
An approximation framework for solvers and decision procedures ⋮ Rigorous roundoff error analysis of probabilistic floating-point computations ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Computer-assisted verification of four interval arithmetic operators ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Polynomial function intervals for floating-point software verification ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions ⋮ Gappa ⋮ Unnamed Item
Uses Software
This page was built for publication: Certification of bounds on expressions involving rounded operators
