Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus, when implementing real-world systems, approximations are inevitable, as are the errors they introduce. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory, energy or runtime, effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff, we need to ensure that the computed results are sufficiently accurate, otherwise we risk disastrously incorrect results or system failures.

In this talk, we present the current state of the tool Daisy which approximates numerical kernels in an automated and trustworthy fashion. Daisy allows a programmer to write exact high-level code and generates an efficient implementation satisfying a given accuracy specification. We discuss Daisy’s verification techniques for bounding the effects of numerical errors, and the approximations Daisy can synthesize fully automatically.

Eva Darulova received a PhD from Ecole Polytechnique Federale de Lausanne (EPFL) and joined the Max Planck Institute for Software Systems (MPI-SWS) as tenure-track faculty in 2015. Her current research focus is on making programming with numerical uncertainties and approximations easier, safer, and the programs themselves more efficient.