Programming with Numerical Uncertainties

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.

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.