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 and categorized into three general
types: 1) dynamic tools, 2) static
tools, 3) commercial tools, and 4)
miscellaneous. You can find tutorials for some of these
tools at fpanalysistools.org.
- CompCert is a compiler that has been formally verified to preserve
floating-point semantics using Coq.
- FLiT: Floating-point Litmus Tests
- FLiT is a test infrastructure for detecting variability in floating-point
code due to differences in compilers and execution environments. It is currently
developed and maintained by Michael Bentley at the University of Utah.
- FPBench is a community benchmark project for floating-point examples.
- FPHPC Bechmark Suite
- This is a collection of programs containing floating-point arithmetic
with the immediate goal of aiding the development and evaluation of
floating-point precision and correctness analysis tools. The long-term goal
is to support and enable the scaling of such tools to provide insights for
high-performance computing (HPC) applications. This collection aims to
address the "middle ground" between real-valued expressions (such as those
contained in the FPBench collection) and full HPC applications.
- KLEE is a symbolic execution virtual machine built on LLVM with a
benchmark suite of example floating-point programs. There is also a
that supports reasoning over floating-point constraints.
- Posit libraries
- Posits are the newest iteration on
John Gustafson's Unum representation
(see below). Unlike Unums, Posits have a fixed overall width but the number
of exponent and significand bits vary according to a run-length-encoded
"regime" field. It provides higher accuracy and a greater dynamic range than
identically-sized IEEE formats.
- Another project from the University of Utah (see FPTaylor and FPTuner
above), S3FP is a tool for finding floating-point inputs that will maximize
- SOAP (Structural Optimisation of Arithmetic Programs) is a tool for
optimizing FPGA-based implementations of floating-point code.
- Sollya is a library and environment for safe floating-point
development, specifically intended to aid the development of math
- Unum library
- Unums ("universal numbers") are a novel binary representation for real
numbers by John Gustafson that exactly
quantifies the uncertainty of a stored value. It extends IEEE floating-point by
making both the exponent and signficand fields variable-sized, and it adds an
"exact" bit that is set if the number is exact and unset if the number
represents a range between representable numbers. It provides a way to obtain
mathematically-rigorous results in numeric code at the cost of computational
- VFLOAT is a a variable-precision floating-point library for FPGAs, developed
and maintained by Miriam Leeser
at Northeastern University.
This list is primarily maintained for the research community by
If you are developing or are maintaining a floating-point tool, or know of a
tool that isn't on the list, please
email the list.