@entry{bec-zyu-mon-18-aa, author = {H Becker and N Zyuzin and R Monat...}, title = {A verified certificate checker for finite-precision error bounds in Coq and HOL4}, journal = {... Formal Methods in ...,}, volume = {}, number = {}, pages = {}, year = 2018, month = , doi = {}, comment = {}, abstract = {}, url = {{\url{https://ieeexplore.ieee.org/abstract/document/8603019/?casa_token=qq6hdmq1CG8AAAAA:Gd4OieeLblljVWKMbT0D4361MUs5AIbkPdsj8nPDu1kTlnk2l_957cvlrLaki65e-RJ55qKe}}}, quotes = {... For the in-logic evaluation in Coq we show range analysis in interval and affine arithmetic, for all other runs we use interval arithmetic. As for the accuracy evaluation, benchmarks ...} }