Real Semantics : Capturing Floating-Point Imprecision

Floating-point numbers and their respective arithmetic operations are often used with the assumption of a certain level of precision. However, there are times when exact precision is necessary. In these cases, floating-point arithmetic is defective in that it is fundamentally interval arithmetic wherein the interval lengths are a function of the median point. Therefore, we present Real Semantics, an automated tool that reasons about the accuracy of floating-point arithmetic. Real Semantics systematically discovers instances where the floating-point arithmetic result is not the most accurate floating-point approximation to the real number implied by any given algorithm. Thereafter, Real Semantics shows the user where the discrepancy is taking place in the form of a line number and variable name.