Programming with Numerical Uncertainties
Speaker(s) : Eva Darulova (Max Planck Institute for Software Systems)
Numerical software, common in scientific computing or embedded systems,
inevitably uses an approximation of the real arithmetic in which most
algorithms are designed. Finite-precision arithmetic, such as fixed-point
or floating-point, is a common and efficient choice, but introduces an
uncertainty on the computed result that is often very hard to quantify. We
need adequate tools to estimate the errors introduced in order to choose
suitable approximations which satisfy the accuracy requirements.
I will present a new programming model where the scientist writes his or
her numerical program in a real-valued specification language with explicit
error annotations. It is then the task of our verifying compiler to select
a suitable floating-point or fixed-point data type which guarantees the
needed accuracy. I will show how a combination of SMT theorem proving,
interval and affine arithmetic and function derivatives yields an accurate,
sound and automated error estimation which can handle nonlinearity,
discontinuities and certain classes of loops.
Additionally, finite-precision arithmetic is not associative so that
different, but mathematically equivalent, orders of computation often
result in different magnitudes of errors. We have used this fact to not
only verify but actively improve the accuracy by combining genetic
programming with our error computation with encouraging results.
More details here
Marc.Mezzarobba (at) nulllip6.fr