Eva Darulova
Talk: Programming with Numerical Uncertainties
- Date and Time
- October 12, 2016 at 3:30pm
- Location
Abstract
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 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.
Bio
Eva Darulova is a tenure-track faculty at the Max Planck Institute for Software Systems. Her research interests include programming languages, software verification and approximate computing and her recent research focused on automated verification and synthesis for numerical programs. She received a PhD from EPFL in 2014 and a BSc degree from University College Dublin in 2009 with a joint major in computer science and mathematical physics.