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

• Final Report Year: 2021

Final Report Abstract

This project extends the static analyzer and synthesizer of approximate numerical programs Daisy in three complementary ways. First, it complements the existing worst-case error analysis with a probabilistic one that allows to provide more nuanced information about numerical errors for applications that can tolerate occasionally larger errors, and that can run on approximate hardware. Second, our project provides a dynamic analysis for real-world and larger scale C/C++ programs that computes necessary information such that the Daisy analyser can be applied to numerically-heavy kernels from the larger applications. Third, we develop code generation and optimization techniques for fixed-point arithmetic implementations of neural network controllers that are increasingly being used in safety critical applications. Overall, our extensions allow Daisy to be effectively applied to a wider range of applications.

Publications

• Sound Probabilistic Numerical Error Analysis, iFM’19
  Debasmita Lohar, Milos Prokop and Eva Darulova
  
• A Two-Phase Approach for Conditional Floating-Point Verification. TACAS’21
  Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis