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
General methods in interval analysis (65G40) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
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