Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

Published in:
Cover of the book

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.

download
DOWNLOAD
share
SHARE
print
PRINT
Metadata
Title
A Two-Phase Approach for Conditional Floating-Point Verification
Authors
Debasmita Lohar
Clothilde Jeangoudoux
Joshua Sobel
Eva Darulova
Maria Christakis
Copyright Year
2021
DOI
https://doi.org/10.1007/978-3-030-72013-1_3