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
- 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
- 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
- BONSAI tests and tunes computational kernels.
- Centre for Next-Generation Arithmetic
- The NGA team develops and promotes the unum number system which is
similar to IEEE 754 format (floating point numbers), but designed to
provide greater performance and accuracy.
- 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.
- Daisy is a framework for accuracy analysis of numerical
programs whose aim is to be modular and extensible.
- 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
- 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
- Gappa helps automated reasoning about floating-point and
fixed-point arithmetic. It has been used to prove
implementations of elementary functions correct.
- Herbie automatically improves the accuracy of floating-point
expressions. Herbie has been used to fix two bugs
- 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
- 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
- A tool for synthesizing error compensation for floating-point programs.
Mike Lam maintains
list on his website, with more detailed descriptions and paper
If you are developing a floating-point tool, or know of one that
isn't on the list,
please email the