8 citations · 20 across the 10 of their papers we have counts for
7 papers · 1 filter
Formally Verified Argument Reduction with a Fused-Multiply-Add
Sylvie Boldo, Marc Daumas, Ren Cang Li
Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accura…
Verified Real Number Calculations: A Library for Interval Arithmetic
Marc Daumas, David Lester, César Muñoz
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a th…
Certification of bounds on expressions involving rounded operators
Marc Daumas, Guillaume Melquiond
Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each boun…
Stochastic Formal Methods for Hybrid Systems
Marc Daumas, David Lester, Erik Martin-Dorel +1
We provide a framework to bound the probability that accumulated errors were never above a given threshold on hybrid systems. Such systems are used for example to model an aircraft…
Stochastic Formal Methods: An application to accuracy of numeric software
Marc Daumas, David Lester
This paper provides a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications…
A library of Taylor models for PVS automatic proof checker
Francisco Cháves, Marc Daumas
We present in this paper a library to compute with Taylor models, a technique extending interval arithmetic to reduce decorrelation and to solve differential equations. Numerical s…