Certification of bounds on expressions involving rounded operators
From MaRDI portal
Publication:2989081
DOI10.1145/1644001.1644003zbMath1364.68328WikidataQ113310518 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 arithmetic; proof system; forward error analysis; Coq; HOL Light; proof obligation; PVS; floating point; dyadic fraction
65G40: General methods in interval analysis
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Uses Software