Automatic Detection of Floating-Point Exceptions

On Friday 8 November 2013, 14:00-15:00 Room B31 of INRIA Lille, Earl Barr (University College London) will give a talk on “Automatic Detection of Floating-Point Exceptions”.



Floating-point exceptions can be disastrous, yet writing exception-free numerical programs is very difficult. In this talk, I will present Ariadne, a practical symbolic execution system specifically designed and implemented for automatically finding witnesses for floating-point exceptions. Ariadne systematically transforms a numerical program to explicitly check each exception-triggering condition, then symbolically executes the transformed program using arbitrary precision rational arithmetic to find candidate inputs that can reach and trigger an exception. Ariadne converts each candidate input into a floating-point number, then tests it against the original program. In general, approximating floating-point arithmetic with arbitrary precision rationals can change paths from feasible to infeasible and vice versa. The key insight of this work is that, for the problem of detecting floating-point exceptions, this approximation works well in practice because, if one input reaches an exception, many are likely to, and at least one of them will do so over both floating-point and arbitrary precision arithmetic. To realize Ariadne, we also devised a novel, practical linearization technique to solve nonlinear constraints. We extensively evaluated Ariadne over 467 scalar functions in the widely used GNU Scientific Library (GSL). Our results show that Ariadne is practical and identifies a large number of real runtime exceptions in GSL.