Automated Rigorous Verification and Synthesis of Approximations
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
(See online at https://doi.org/10.1007/978-3-030-34968-4_18) - A Two-Phase Approach for Conditional Floating-Point Verification. TACAS’21
Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis
(See online at https://doi.org/10.1007/978-3-030-72013-1_3)
