methodes-formelles sise sycomores

Towards Reliable and Efficient Numerical Code through Sound Optimizations

26 mars 2026 à 10h

Anastasia Isychev

Anastasia Isychev, postdoc at TU Wien

Abstract:

Numerical software is notoriously difficult to get right. Finite-precision computations do not follow real-valued arithmetic rules and can therefore exhibit unintended behavior, in particular, due to rounding errors. Finding an implementation that is not only accurate but also efficient is challenging for non-expert users. Sound optimizers for numerical kernels aim to improve either accuracy or performance while providing guarantees on the worst-case rounding error bound of the optimized program. However, due to the abstractions and over-approximations required for soundness, these optimizers tend to be overly conservative.

This talk addresses this aspect in two ways. First, it presents regime inference, a technique that improves existing sound optimizations by exploiting the uneven distribution of rounding errors across a program’s input domain. The algorithm partitions the domain into regimes and infers optimized expressions for each region, enabling more aggressive optimizations while preserving global accuracy guarantees. Secondly, it highlights the differences in effectiveness in sound static and unsound dynamic optimizers for floating-point programs.

En savoir plus...

Salle Atrium, bâtiment ESPRIT

Plus d'actualités