The pitfalls of verifying floating-point computations

Abstract

Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.

References in corpus (1)

• A Static Analyzer for Large Safety-Critical Software

Cited by in corpus (14)

• Automatic Modular Abstractions for Template Numerical Constraints
• CLAID: Closing the Loop on AI & Data Collection -- A Cross-Platform Transparent Computing Middleware Framework for Smart Edge-Cloud and Digital Biomarker Applications
• Finding Root Causes of Floating Point Error with Herbgrind
• The Trusted Computing Base of the CompCert Verified Compiler
• An Open Source C++ Implementation of Multi-Threaded Gaussian Mixture Models, k-Means and Expectation Maximisation
• Influence of round-off errors on the reliability of numerical simulations of chaotic dynamic systems
• Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification
• Agatha: Smart Contract for DNN Computation
• A Practical Approach to Interval Refinement for math.h/cmath Functions
• Towards platform-independent verification of the standard mathematical functions: the square root function
• Extracting efficient exact real number computation from proofs in constructive type theory
• Internal versus external balancing in the evaluation of graph-based number types
• Abstract Compilation for Verification of Numerical Accuracy Properties
• Concrete Semantics of Programs with Non-Deterministic and Random Inputs