The floatingpoint 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, and
many of the reducedprecision tools were compared in a
recent survey by authors from
the Polytechnic University of Milan.
Tools on the list are not endorsed, and need not endorse or
support the FPBench project. The list is intended to be
exhaustive.
Additionally, the
FPBench project
provides benchmarks,
compilers,
and standards for floatingpoint
research tools.
Dynamic Tools
 ADAPT
 ADAPT (Automatic Differentiation Applied to Precision Tuning) is a tool
developed by Mike Lam from JMU
and Harshitha Menon from LLNL. It
uses the reverse mode of algorithmic differentiation to determine how much
precision is needed in a program's inputs and intermediate results in order
to achieve a desired accuracy in its output, converting this information
into precision recommendations.

 AMP
 AMP (Automated Mixed Precision) is a tool developed by Ralph Nathan and
Daniel Sorin (Duke University)
for mixedprecision analysis. It begins with a singleprecision version of a
program and uses a variety of metrics and heuristics to gradually raise certain
portions of the program to higher precision in order to achieve the desired
accuracy in the outputs.

 AMPTGA
 AMPTGA is a tool developed by a multiinstitutional team for automated
sourcelevel mixedprecision for GPU applications, combining various static and
dynamic analysis approaches.

 Atomu
 Atomu is a tool
developed by Daming Zou
(Peking University) that uses "atomic" condition numbers of individual
floatingpoint operations to estimate the introduced error. It also performs
an evolutionary search to find inputs that trigger the highest condition
number for each operation. The instrumentation portion of the tool is
implemented as an LLVM pass.

 CADNA / PROMISE
 CADNA (Control of Accuracy and Debugging for Numerical Applications)
estimates roundoff errors by replacing floatingpoint arithmetic with
discrete stochastic arithmetic (DSA), essentially modeling error using
randomized rounding (up or down) instead of roundtonearesteven. A new tool
called PROMISE (PRecision OptiMISE) uses this technique to perform a
deltadebugging search and report mixed precisions for C and C++ programs.

 CRAFT
 CRAFT (Configurable Runtime Analysis for FloatingPoint Tuning) was
originally a framework based on the Dyninst
binary analysis toolkit to perform various dynamic floatingpoint analyses,
including cancellation detection, dynamic range tracking, and automated
mixedprecision analysis. CRAFT can perform an automated search of a
program's instruction space, determining the level of precision necessary in
the result of each instruction to pass a userprovided verification routine
assuming all other operations are done in double precision. This gives a
general overview of the approximate precision requirements of the program,
providing insights and guidance for mixedprecision implementation.

 There is a branch of CRAFT by Andrew Shewmaker (OpenEye Scientific,
formerly LANL) that adds a new analysis mode for extracting histograms of
all floatingpoint values encountered during a program run. He has also been
building a variant of this tool based on SHVAL (described below).

 FloatSmith
 FloatSmith is an integration project that provides automated
sourcetosource tuning and transformation of floatingpoint code for mixed
precision using three existing tools: 1) CRAFT, 2) ADAPT, and 3) TypeForge. The
primary search loop is guided by CRAFT and uses TypeForge to prototype
mixedprecision versions of an application. ADAPT results can optionally be used
to help narrow the search space, and there are a variety of options to customize
the search.

 FPDetect
 FPDetect is a tool from the University of Utah for synthesizing error
detectors for stencil applications. It begins with an offline phase where
affine analysis is used to tighly estimate the floatingpoint precision
preserved across computations for intervals of data points. This bound along
with an auxiliary direct evaluation technique is then utilized to
instantiate optimally situated detectors across the compute space when
executing online. Violations of this bound can be attributed with certainty
to errors such as softerrors or logical bugs.

 FPDiff
 FPDiff is a tool by Jackson Vanover (UC Davis) that performs automated
differential testing on mathematical library source code, extracting
numerical function signatures, synthesizing drivers, creating equivalence
classes of synonymous functions, and executing tests to detect meaningful
numerical discrepancies between implementations.

 FPED
 FPED is a dynamic analysis that detects arithmetic expression errors
using MPFR and test set generation.

 FPGen
 FPGen is a tool by Hui Guo
(UC Davis) that uses symbolic execution to generate inputs that maximize numerical error,
finding more errors than S3FP or KLEE.

 Paper: "Efficient Generation of ErrorInducing FloatingPoint Inputs via Symbolic Execution" (to appear, ICSE'20)
 Source: github.com/ucdplse/fpgen
 fpPrecisionTuning
 fpPrecisionTuning is a combination of two Python tools (C2mpfr and
DistributedSearch) that together can be used to find mixedprecision versions
of C programs. Like CRAFT and Precimonious, this tool performs a search over
the mixedprecision search space using a usergiven error bound, but this tool
uses MPFR and source code modification to simulate nonstandard precisions. The
authors have applied this toolchain to a variety of examples from different
domains including fixedprecision computations on an FPGA.

 FPSpy
 FPSpy is a tool by Peter Dinda
(Northwestern) that uses several different forms of runtime analysis to
detect and measure various floatingpoint issues. It is implemented as an
LD_PRELOAD
library and works on unmodified x64 executables,
monitoring floatingpoint exceptions and other events of interest to
report results with varying levels of granularity and overhead.

 GPUFPtuner
 GPUFPtuner is a mixedprecision autotuner for GPU applications, built
on top of the Rose compiler framework.

 GPUMixer
 GPUMixer is a tool written by a multiinstitutional team for LLVMbased
mixedprecision analysis that is performancefocused, looking for potential
speedups first and then verifying their accuracy afterwards.

 Herbie
 Herbie automatically improves the accuracy of floatingpoint
expressions. Herbie has been used to fix two bugs in
math.js, and it also provides a
web interface.

 The authors of Daisy and Herbie have worked together to
combine their tools:

 Herbgrind
 Herbgrind is a dynamic analysis tool for binaries (built on Valgrind)
to help find the root cause of floatingpoint error in large programs.

 HiFPTuner
 HiFPTuner is an extension of Precimonious (see below) that uses dependence
analysis and edge profiling to enable a more efficient hierarchical search
algorithm for mixedprecision configurations.

 pLiner
 pLiner is a tool for automatically identifying code that will trigger
compilerinduced numerical variability. It works by combining selective
precision enhancements and a guided dynamic search, decreasing the amount
of time required to detect issues.

 PositDebug / FPSanitizer
 PositDebug and FPSanitizer are tools from the Rutgers Architecture and
Programming Languages group. Both use LLVMbased instrumentation and MPFR
shadow values to check Posit (the former) and regular floatingpoint code
(the latter). This approach is faster than the Valgrindbased
instrumentation used by Herbgrind.

 Precimonious
 Precimonious is a tool written by Cindy Rubio González (currently UC
Davis) that leverages the LLVM framework to tweak
variable declarations to build and prototype mixedprecision configurations.

 More recent work uses shadow value analysis to speed up the search.

 PyFloT
 PyFloT is a tool for mixedprecision tuning of applications using an
instructioncentric analysis that uses call stack information and temporal
locality to address the large scale of HPC scientific programs. PyFloT
supports applications written in a combination of Python, CUDA, C++, and
Fortran.

 Shaman
 Shaman is a library that uses operator overloading and errorfree
transformations to track numerical error thorough computations by
replacing floatingpoint numbers with instrumented alternatives. It can
evaluate the number of significant digits of any floatingpoint number in
a computation and has been designed with a focus on highperformance
computating and simulation. It is compatible with mixed precision and
parallelism and does not interfere with the control flow of the program.

 SHVAL
 SHVAL (SHadow Value Analysis Library) is a tool by
Mike Lam that uses the
Intel Pin
instrumentation framework to perform full heavyweight shadowvalue analysis for
floatingpoint arithmetic, effectively allowing developers to simulate any
realnumbered representation for which a plugin can be developed.

 This work was extended by Ramy Medhat (U. of Waterloo) to perform
peraddress or perinstruction floatingpoint error analysis. Using this
framework, he developed several mixedprecision versions of an image processing
library, demonstrating how the tool can assist with making performance, energy,
and accuracy tradeoffs in the embedded domain.

 STOKE
 STOKE is a general stochastic
optimization and program synthesis tool from Stanford that has been extended
to handle floatingpoint computation. STOKE can trade off accuracy for
performance for floatingpoint computations.

 Verificarlo
 Verificarlo is a tool written by Pablo de
Oliveira Castro (Université de Versailles StQuentinenYvelines), Eric
Petit, and Christophe Denis (ENS Cachan). It leverages the LLVM
framework for automated Monte Carlo Arithmetic analysis.

 VeriTracer
 Verificarlo (see above) has recently been extended by Yohan Chatelain,
including the addition of contextual information as well as a temporal
visualization tool called VeriTracer.

 Verrou
 Verrou is a Valgrindbased tool written by François Févotte and others from
EDT in France. The tool can simulate choosing a random rounding mode for every
operation, and performs a delta debugging search to find areas of code that fail
a userprovided verification routine under this scheme. It can also use the
Verificarlo frontend (see above) for lower overhead.

Static Tools
 Alive / LifeJacket
 Alive verifies that LLVM IR optimizations don't change program
behavior, and includes support for floatingpoint instructions in
an extension named LifeJacket. Alive has verified 43 LLVM
optimizations and discovered eight incorrect ones.

 Alive
 AliveNJ verifies that LLVM IR optimizations don't change
program behavior, and includes support for floatingpoint
instructions. AliveNJ has found five bugs in LLVM optimization
passes.

 cohd / syhd
 Laurent Thévenoux at LIP, ENS de Lyon has written tools for sourcetosource
error compensation and synthesis of floatingpoint code.

 Daisy
 Daisy is another tool by Eva
Darulova (the author of Rosa, see below) that combines various types
of static and dynamic analysis of floatingpoint code and is designed to be
modular and extensible. Eva also has a paper with Anastasiia Izycheva on
computing sound relative errors. They find that this can produce much
tighter error bounds than analyzing absolute error, and an implementation is
included in Daisy. Finally, Eva has a paper with Einar Horn and Saksham
Sharma on mixedprecision tuning in Scala and C, which is also included in
Daisy.

 The authors of Daisy and Herbie have worked together to
combine their tools:

 dco / scorpio
 A group from CERTH & University of Thessaly and RWTH Aachen have written
a significance analysis system using a combination of interval arithmetic and
automatic differentiation. The software does not yet seem to be publicly
available.

 ESBMC
 The Efficient SMTbased Bounded Model Checker (ESBMC) is an SMTbased
model checker for single and multithreaded C/C++ programs with support for
floatingpoint arithmetic.

 Flocq
 Flocq is a floatingpoint formalization for Coq, written by
Sylvie Boldo and
others. It provides a library of theorems for analyzing arbitraryprecision
floatingpoint arithmetic.

 FPhile
 Floatingpoint stability analysis via SMT solving and theorem proving.

 FPSyn
 FPSyn is an implementation of a floatingpoint predicate synthesis
technique that automatically derives an expression to calculate the
roundoff error bound of the input computation.

 FPTaylor / FPTuner
 A group at the University of Utah describes a way of using partial
derivatives and symbolic Taylor series expansions to bound floatingpoint
roundoff error; this achieves much tighter bounds than interval/affine/SMT
methods. More recently, they have extended theird work by performing a broad
comparison of many error bounding analyses.

 They have also built a mixedprecision tool for Python code based on this
technique. Note that it also requires the commercial
Gurobi Optimizer.

 Gappa
 Gappa helps automated reasoning about floatingpoint and
fixedpoint arithmetic. It has been used to prove the CRlibm
implementations of elementary functions correct.

 moTuner
 moTuner is a framework built on LLVM for efficiently tuning
mixedprecision operators during compilation.

 POP
 POP (Precision OPtimizer) is a tool written by Dorra Ben Khalifa
(Laboratory of Mathematics and Physics, University of Perpignan Via Domitia)
that uses abstract interpretation to determine the minimal precision
required on inputs. The primary current contribution is the application of
these techniques to the Internet of Things (IoT) domain.

 PRECiSA / FPRoCK
 PRECiSA (Program Roundoff Error Certifier via Static Analysis) is a
tool from the NIA and NASA that calculates symbolic error
bounds using the PVS language. The authors
also provide a web interface. More recently, the FPRoCK tool was written in
collaboration with authors at the University of Utah to solve mixed real and
floatingpoint programs, which improved the accuracy of PRECiSA.

 Real2Float
 Victor Magron and others present a framework for providing upper bounds on
absolute roundoff errors using semidefinite programming and sums of squares
certificates. The results can be checked using the Coq theorem prover.

 Rosa
 Rosa is a sourcetosource translator written by Eva Darulova (now at MPISWS,
previously EPFL) for the Scala language. It uses an SMT solver to annotate a
program with mixedprecision types.

 Salsa
 Salsa is an abstractinterpretationbased floatingpoint analysis tool that
suggests transformations to minimize floatingpoint error, and is the dissertation
work of Nasrine Damouche. The source code is not available.

 Satire
 Satire is a sound rounding error analysis and estimator that uses
several techniques like path strength reduction and bound optimization to
improve the scalability of static analysis. This analysis scales to hundreds
of thousands of operations.

 TAFFO
 TAFFO is an LLVMbased conversion and autotuning framework that tries
to replace floatingpoint operations with fixedpoint operations to the
extent possible.

 VP Float
 VP Float is an extension of the C type system to represent
variableprecision floatingpoint arithmetic. The extension is built using
LLVM and has two backend code generators, one for a RISCV coprocessor and one
for the GNU MPFR multiprecision library.

Commercial Tools
 Astrée
 Astrée is a commercial static analysis tool for proving the correctness
of C code, including all floatingpoint computation. It has been used to
prove the absence of runtime exceptions in flight control software for
Airbus planes.

 Fluctuat
 Fluctuat is a commercial, abstractinterpretationbased static analysis tool
for analyzing numerical code in C or Ada and characterizing the errors
caused by the approximation inherent in floatingpoint arithmetic. Fluctuat
has been used to verify safetycritical embedded systems. It was originally
written by Eric Goubault, Matthieu Martel, and Sylvie Putot.

 Numalis Software Suite
 Numalis Software Suite is a collection of several commercial tools for
static and dynamic analysis of floatingpoint code with the goal of
generating more accurate codes and making mixedprecision decisions,
targeted primarily at AI and neural network domains.

Miscellaneous
 CompCert
 CompCert is a compiler that has been formally verified to preserve
floatingpoint semantics using Coq.

 Fbench / Ffbench
 Fbench and Ffbench are two floatingpoint performance benchmarks by
John Walker (Fourmilab).

 FLiT: Floatingpoint Litmus Tests
 FLiT is a test infrastructure for detecting variability in floatingpoint
code due to differences in compilers and execution environments. It is currently
developed and maintained by Michael Bentley at the University of Utah.

 FPBench
 FPBench is a community benchmark project for floatingpoint examples.

 FPHPC Bechmark Suite
 This is a collection of programs containing floatingpoint arithmetic
with the immediate goal of aiding the development and evaluation of
floatingpoint precision and correctness analysis tools. The longterm goal
is to support and enable the scaling of such tools to provide insights for
highperformance computing (HPC) applications. This collection aims to
address the "middle ground" between realvalued expressions (such as those
contained in the FPBench collection) and full HPC applications.

 FPVM
 FPVM is a floatingpoint virtual machine proposed and prototyped by
Peter Dinda and others at Northwestern University. The goal is to allow an
existing application binary to be extended to support alternative
arithmetic systems. The current implementation combines static binary
analysis with trapandemulate execution.

 KLEE
 KLEE is a symbolic execution virtual machine built on LLVM with a
benchmark suite of example floatingpoint programs. There is also a
fork
that supports reasoning over floatingpoint 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 runlengthencoded
"regime" field. It provides higher accuracy and a greater dynamic range than
identicallysized IEEE formats.

 S3FP
 Another project from the University of Utah (see FPTaylor and FPTuner
above), S3FP is a tool for finding floatingpoint inputs that will maximize
error.

 SOAP
 SOAP (Structural Optimisation of Arithmetic Programs) is a tool for
optimizing FPGAbased implementations of floatingpoint code.

 Sollya
 Sollya is a library and environment for safe floatingpoint
development, specifically intended to aid the development of math
library functions.

 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 floatingpoint by
making both the exponent and signficand fields variablesized, 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
mathematicallyrigorous results in numeric code at the cost of computational
efficiency.

 VFLOAT
 VFLOAT is a a variableprecision floatingpoint library for FPGAs, developed
and maintained by Miriam Leeser
at Northeastern University.

This list is primarily maintained for the research community by
Mike Lam.
If you are developing or are maintaining a floatingpoint tool, or know of a
tool that isn't on the list, please
email the list.