Automated Rigorous Verification and Synthesis of Approximations

• Applicant: Eva Darulova, Ph.D.
• Subject Area: Software Engineering and Programming Languages
• Term: from 2017 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 387674182

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 introduced by them. 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.The goal of this project is to develop an end-to-end system which approximates numerical programs in an automated and trustworthy fashion. The programmer will be able to write exact high-level code and our 'approximating compiler' will generate an efficient implementation satisfying a given accuracy specification. In order to achieve this vision, we will develop novel sound techniques for verifying the accuracy of approximate numerical programs, as well as new synthesis approaches to generate such approximations automatically.

• DFG Programme: Research Grants