Abstract

Computational science code makes intense use of floating-point numbers. Unfortunately, powerful constraint-based analysis techniques rarely support floating point, or they scale poorly to this domain. In this talk, I will discuss our experience developing techniques that can reason about floating-point constraints. These include methods that make use of the theory of floating point offered by some SMT solvers, solving floating-point constraints via fuzzing, and approximating floating point via fixed point.

Based on joint work with Cristian Cadar, Daniel Liew, Daniel Schemmel, Alastair Donaldson, Rafael Zähl, Klaus Wehrle, Thom Hughes, Martin Nowack, J. Ryan Stinnet.