Eva Darulova, EPFL, Switzerland

"Programming with Numerical Uncertainties"

(Vortrag im Rahmen der "MPI Distinguished Lecture Series" in Kooperation mit dem Fachbereich Informatik)

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. We have further combined our error computation with genetic programming to not only verify but also improve accuracy. Finally, together with techniques from validated numerics we developed a runtime technique to certify solutions of nonlinear systems of equations, quantifying truncation in addition to roundoff errors.

Bio: Eva Darulova is a postdoc at EPFL in the Laboratory for Automated Reasoning and Analysis. Her research interests include programming languages, software verification and in particular approximate computing. Her recent research focused on automated verification and synthesis for numerical programs where she developed techniques and tools for explicit handling of uncertainties. She received a PhD from EPFL in 2014 and a BS degree from University College Dublin in 2009 with a joint major in computer science and mathematical physics.