forked from FPBench/fpbench.org
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcommunity.html
157 lines (127 loc) · 6.97 KB
/
community.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
<!doctype html>
<html>
<head>
<meta charset="utf-8"/>
<title>Community Tools</title>
<link rel="stylesheet" type="text/css" href="fpbench.css">
</head>
<body>
<header>
<a href='.' style='color: black; text-decoration: none;'>
<img src='img/logo.png' height='150' alt='FPBench Logo' />
<h1>Community Tools</h1>
<p>Tools from the Floating-point Research World</p>
</a>
</header>
<p>
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.
</p>
<p><em>Tools on the list are not endorsed, and need not endorse or
support the FPBench project.</em> The list is intended to be
exhaustive.</p>
<dl class="tools-list">
<dt><a href="https://github.com/4tXJ7f/alive">Alive</a></dt>
<dd>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.</dd>
<dt><a href="https://github.com/rutgers-apl/alive-nj">Alive-NJ</a></dt>
<dd>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.</dd>
<dt><a href="http://www.astree.ens.fr/">Astrée</a></dt>
<dd>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.</dd>
<dt><a href="https://bitbucket.org/icl/bonsai">BONSAI</a></dt>
<dd>BONSAI tests and tunes computational kernels.</dd>
<dt><a href="http://www.posithub.org">Centre for Next-Generation Arithmetic</a></dt>
<dd> 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. </dd>
<dt><a href="https://hal.archives-ouvertes.fr/hal-01158399">cohd</a></dt>
<dd>cohd is a tool for source-to-source error compensation of floating-point programs.</dd>
<dt><a href="http://compcert.inria.fr/index.html">CompCert</a></dt>
<dd>CompCert is a formally-verified compiler for C, including support for floating-point.</dd>
<dt><a href="https://github.com/malyzajko/daisy">Daisy</a></dt>
<dd>Daisy is a framework for accuracy analysis of numerical
programs whose aim is to be modular and extensible.</dd>
<dt><a href="http://pruners.github.io/flit">FLiT</a></dt>
<dd>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.</dd>
<dt><a href="http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/fluctuat.html">Fluctuat</a></dt>
<dd>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.</dd>
<dt><a href="https://sites.google.com/site/fptaylordemo/">FPTaylor</a></dt>
<dd>FPTaylor provides rigorous and accurate bounds on the size of
round-off errors in a floating-point computations.</dd>
<dt><a href="https://github.com/soarlab/FPTuner">FPTuner</a></dt>
<dd>FPTuner chooses the precision that will compute a
floating-point expression with maximum speed while achieving an
error bound.</dd>
<dt><a href="http://gappa.gforge.inria.fr/">Gappa</a></dt>
<dd>Gappa helps automated reasoning about floating-point and
fixed-point arithmetic. It has been used to prove
the <a href="https://gforge.inria.fr/scm/browser.php?group_id=5929&extra=crlibm">CRlibm</a>
implementations of elementary functions correct.</dd>
<dt><a href="https://herbie.uwplse.org">Herbie</a></dt>
<dd>Herbie automatically improves the accuracy of floating-point
expressions. Herbie has been used to fix two bugs
in <a href="http://mathjs.org/">math.js</a>.</dd>
<dt><a href="http://herbgrind.ucsd.edu/">Herbgrind</a></dt>
<dd>Herbgrind is a dynamic analysis tool for binaries to help find
the root cause of floating-point error in large programs.</dd>
<dt><a href="http://www.ti3.tu-harburg.de/rump/intlab/">IntLab</a></dt>
<dd>IntLab is a fast implementation of interval arithmetic for
Matlab and Octave. IntLab focuses on the provable correctness of
its results and on speed.</dd>
<dt><a href="https://github.com/srg-imperial/klee-float">KLEE-float</a></dt>
<dd>A version of the KLEE symbolic execution engine that is designed to support reasoning over floating-point constraints.</dd>
<dt><a href="https://github.com/corvette-berkeley/precimonious">Precimonious</a></dt>
<dd>Precimonious finds parts of a program where lower
floating-point precision can be used, thus making the program
faster, without violating accuracy constraints.</dd>
<dt><a href="http://precisa.nianet.org/">PRECiSA</a></dt>
<dd>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.</dd>
<dt><a href="http://nl-certify.forge.ocamlcore.org/real2float.html">Real2Float</a></dt>
<dd>Real2Float can provide upper bounds for floating-point
round-off errors using several different optimization
techniques.</dd>
<dt><a href="http://formalverification.cs.utah.edu/grt/">S3FP</a></dt>
<dd>S3FP searches for inputs that cause floating-point expressions
to have high round-off error.</dd>
<dt><a href="http://perso.univ-perp.fr/nasrine.damouche/Salsa/">Salsa</a></dt>
<dd>Salsa improves the accuracy of floating-point computations
using static analysis.</dd>
<dt><a href="https://github.com/admk/soap">SOAP</a></dt>
<dd>SOAP automatically explores the tradeoff in error, die area,
and latency for FPGA implementations of floating-point functions
expressed as C programs.</dd>
<dt><a href="http://stoke.stanford.edu/">STOKE</a></dt>
<dd>STOKE is a optimizer and program synthesizer for x86-64 binary
code. STOKE can trade off accuracy for performance for
floating-point computations.</dd>
<dt><a href="https://hal.archives-ouvertes.fr/hal-01236919">syhd</a></dt>
<dd>A tool for synthesizing error compensation for floating-point programs.</dd>
</dl>
<p>Mike Lam maintains
a <a href="https://w3.cs.jmu.edu/lam2mo/fpanalysis.html">similar
list</a> on his website, with more detailed descriptions and paper
links.</p>
<p>If you are developing a floating-point tool, or know of one that
isn't on the list,
please <a href="mailto:[email protected]">email the
list</a>.</p>
</body>
</html>