A compiler for sound floating-point computations, Joao Rivera (ETH Zurich)

Thursday, January 26, 2023
Location: Scott 6142
Time: 4:00PM-5:00PM

Floating-point arithmetic is widely used in scientific and engineering applications but is unsound, i.e., there is no guarantee on the accuracy obtained. When working with floating-point, developers often use it as a proxy for real arithmetic and expect close to exact results. Unfortunately, while often true, the result may also deviate due to round-off errors. Their non-intuitive nature makes it hard to predict when and how these errors accumulate to the extent that they invalidate the final result. In this talk, we discuss an automatic approach to soundly bound such uncertainties using interval arithmetic and affine arithmetic. We present a source-to-source compiler that translates a C program performing floating-point computations to an equivalent C program with soundness guarantees, i.e., the generated program yields a precision certificate on the number of correct bits in the result. We will briefly discuss the design and implementation of our compiler, followed by techniques used to improve the accuracy of the result.

Joao Rivera is a PhD student in Computer Science at ETH Zurich where he is advised by Prof. Markus Püschel (ETHZ) and co-supervised by Prof. Franz Franchetti (CMU). His research focuses on applying compiler techniques and static analysis to improve the accuracy and performance of reliable floating point computations. Prior to joining ETH, he received his M.Sc. in Embedded Systems from the Eindhoven University of Technology.