An overview of semantics for the validation of numerical programs

Interval computations, stochastic arithmetic, automatic differentiation, etc.: much work is currently done to estimate and to improve the numerical accuracy of programs but few comparative studies have been carried out. In this article, we introduce a simple formal semantics for floating point numbers with errors which is expressive enough to be formally compared to the other methods. Next, we define formal semantics for interval, stochastic, automatic differentiation and error series methods. This enables us to formally compare the properties calculated in each semantics to our reference, simple semantics. Most of these methods having been developed to verify numerical intensive codes, we also discuss their adequacy to the formal validation of softwares and to static analysis. Finally, this study is completed by experimental results.