Herbie

"The Herbie project provides Herbie and Herbgrind, complementary tools for finding and fixing floating point problems:

Herbie

rewrites floating point expressions to make them more accurate. Herbie supports all commonly-used floating point functions, and uses a cutting-edge search to identify more-accurate rearrangements of a floating point computation.

Herbgrind

analyzes binaries to catch floating point inaccuracies as they occur and extract them for analysis. Herbgrind analyzes binaries directly, detecting problems on realistic workloads and extracting them in a standard format.

The Herbie tools have been used on large numerical computations, mathematical libraries, graphics programs, and embedded systems. It regularly finds subtle floating point issues and produces fixes.

Herbie depends on Racket, a dynamic language developed by Northeastern University. To install Herbie, one must first install Racket. Once Racket is installed, Herbie should run without problems.

http://herbie.uwplse.org/

http://uwplse.org/#projects