FPBench Logo

Community Tools

Tools from the Floating-point Research World

The floating-point research community has developed many tools that authors of numerical software can use to test, analyze, or improve their code. They are listed here in alphabetical order.

Tools on the list are not endorsed, and need not endorse or support the FPBench project. The list is intended to be exhaustive.

Alive verifies that LLVM IR optimizations don't change program behavior, and includes support for floating-point instructions in an extension named LifeJacket. Alive has verified 43 LLVM optimizations and discovered eight incorrect ones.
Alive-NJ verifies that LLVM IR optimizations don't change program behavior, and includes support for floating-point instructions. Alive-NJ has found five bugs in LLVM optimization passes.
Astreé is a static analysis tool for C that can prove the absence of runtime exceptions, including in the presence of floating-point operations. It has been used to prove the absence of runtime exceptions in flight control software for Airbus planes.
BONSAI tests and tunes computational kernels.
Daisy is a framework for accuracy analysis of numerical programs whose aim is to be modular and extensible.
cohd is a tool for source-to-source error compensation of floating-point programs.
CompCert is a formally-verified compiler for C, including support for floating-point.
FLiT is a reproducibility testing framework that verifies floating-point code under different compilers and compiler optimizations. It finds which compilations change the result of your floating-point code.
Fluctuat is a static analysis tool for C that can characterize the errors caused by the approximation inherent in floating-point arithmetic. Fluctuat has been used to verify safety-critical embedded systems.
FPTaylor provides rigorous and accurate bounds on the size of round-off errors in a floating-point computations.
FPTuner chooses the precision that will compute a floating-point expression with maximum speed while achieving an error bound.
Gappa helps automated reasoning about floating-point and fixed-point arithmetic. It has been used to prove the CRlibm implementations of elementary functions correct.
Herbie automatically improves the accuracy of floating-point expressions. Herbie has been used to fix two bugs in math.js.
Herbgrind is a dynamic analysis tool for binaries to help find the root cause of floating-point error in large programs.
IntLab is a fast implementation of interval arithmetic for Matlab and Octave. IntLab focuses on the provable correctness of its results and on speed.
A version of the KLEE symbolic execution engine that is designed to support reasoning over floating-point constraints.
Precimonious finds parts of a program where lower floating-point precision can be used, thus making the program faster, without violating accuracy constraints.
PRECiSA is a fully-automatic static analysis tool for estimating the round-off error of floating-point first-order functional programs in the PVS language.
Real2Float can provide upper bounds for floating-point round-off errors using several different optimization techniques.
S3FP searches for inputs that cause floating-point expressions to have high round-off error.
Salsa improves the accuracy of floating-point computations using static analysis.
SOAP automatically explores the tradeoff in error, die area, and latency for FPGA implementations of floating-point functions expressed as C programs.
STOKE is a optimizer and program synthesizer for x86-64 binary code. STOKE can trade off accuracy for performance for floating-point computations.
A tool for synthesizing error compensation for floating-point programs.

Mike Lam maintains a similar list on his website, with more detailed descriptions and paper links.

If you are developing a floating-point tool, or know of one that isn't on the list, please email the list.