Scalable Error Verification: How Accurate is your Numerical Code?

The goal of this project is to develop the first rigorous general-purpose error analysis for real-world numerical software to compute a guaranteed bound on finite-precision rounding errors and errors due to noisy inputs.

It will be implemented in the LLVM compiler framework and thus widely applicable to a variety of different languages including C/C++, Rust and Scala.

The numerical error bounds computed by our analysis will contribute to ensuring the correctness and safety of numerical software in different domains, including embedded systems and scientific computing.

Furthermore, our analysis will enable resource savings by permitting to safely reduce the precision of numerical computations.We will achieve this goal by developing a new foundation for automated static analysis of rounding errors based on deductive relational verification. This is an established technique, but has so far seen limited support for floating-point arithmetic.

We furthermore take a holistic view and consider the practical usability of our approach by developing and integrating function specification inference into our proposed workflow.

Overall this project addresses two long-standing challenges in deductive software analysis: floating-point reasoning and specification inference.