ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Wed 8 Jun 2022 13:30 - 13:50 at Aurora Borealis 1 - Verification and Compilation Chair(s): Alexander J. Summers

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 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Verification and CompilationResearch Papers / Hub Talks at Aurora Borealis 1
Chair(s): Alexander J. Summers University of British Columbia
13:30
20m
Talk
A Compiler for Sound Floating-Point ComputationsHub Talk
Hub Talks
Joao Rivera ETH Zurich, Franz Franchetti Carnegie Mellon University, USA, Markus Püschel ETH Zurich
Link to publication DOI
13:50
20m
Talk
Verified Compilation and Optimization of Floating-Point Programs in CakeMLArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Heiko Becker MPI-SWS, Robert Rabe TU Munich, Eva Darulova Uppsala University, Magnus O. Myreen Chalmers University of Technology, Zachary Tatlock University of Washington, Ramana Kumar DeepMind, Yong Kiam Tan Carnegie Mellon University, Anthony C. J. Fox Arm Limited
14:10
20m
Talk
REST: Integrating Term Rewriting with Program VerificationArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Zachary Grannan University of British Columbia, Eva Darulova Uppsala University, Alexander J. Summers University of British Columbia, Niki Vazou IMDEA Software Institute
14:30
20m
Talk
Defining Corecursive Functions in Coq Using ApproximationsVCOOP 2022ECOOP 2022
Research Papers
Vlad Rusu Inria, Lille, France, David Nowak CRIStAL, CNRS & University of Lille