Open Access 2021 | OriginalPaper | Chapter
A Two-Phase Approach for Conditional Floating-Point Verification
Authors : Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis
Published in: Tools and Algorithms for the Construction and Analysis of Systems
Publisher: Springer International Publishing
Tools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.