Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Programming with Numerical Uncertainties
Speaker:Dr. Eva Darulova
coming from:EPFL, Switzerland
Speakers 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.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Tuesday, 17 February 2015
Time:10:30
Duration:90 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
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 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.

Contact
Name(s):Vera Laubscher
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
  • Vera Laubscher, 02/11/2015 09:46 AM
  • Vera Laubscher, 02/10/2015 04:08 PM -- Created document.