The pitfalls of verifying floating-point computations

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

• Type: Journal
• Year: 2008
• Where: TOPLAS
• Authors: David Monniaux
• Keywords: Current Critical Systems, Floating-point Computations, Static Analysis, TOPLAS 2008