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. 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 performance and accuracy of the result.
Wed 8 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00
|A Compiler for Sound Floating-Point ComputationsHub Talk|
Hub TalksLink to publication DOI
|Verified Compilation and Optimization of Floating-Point Programs in CakeMLVCOOP 2022ECOOP 2022|
|REST: Integrating Term Rewriting with Program VerificationVCOOP 2022ECOOP 2022|
|Defining Corecursive Functions in Coq Using ApproximationsVCOOP 2022ECOOP 2022|