Daisy - a framework for sound accuracy analysis and optimization of numerical programs

By Eva Darulova
Video conference

Abstract
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. Unfortunately, the current way of programming with approximations is mostly manual, and consequently costly, error prone and often produces suboptimal results.

In this talk, we present the current state of the tool Daisy which approximates numerical programs 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.

Bio
Eva Darulova obtained her PhD from EPFL in 2014. Since 2015, she is a tenure-track faculty at the Max Planck Institute for Software Systems in Germany. Her research interests include programming languages, software verification and approximate computing. Recently, she has also been involved with programming robots.

More information