-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathfm18.html
61 lines (54 loc) · 2.48 KB
/
fm18.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
<!doctype html>
<html>
<head>
<meta charset="utf-8"/>
<title>FPBench at FM’18</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>FPBench at FM’18</h1>
</a>
<p>Combining Tools for Optimization and Analysis of Floating-Point Computations</p>
<ul>
<li><a href="index.html">Home</a></li>
<li><a href="benchmarks.html">Benchmarks</a></li>
<li><a href="https://github.com/FPBench/FPBench/blob/main/tools.md">Compilers</a></li>
<li><a href="spec/index.html">Standards</a></li>
</ul>
</header>
<p>The second paper on <a href="./">FPBench</a> was published at the
Formal Methods conference in 2018.</p>
<h2>Abstract</h2>
<blockquote class="abstract">
Recent renewed interest in optimizing and analyzing floating-point
programs has lead to a diverse array of new tools for numerical programs.
These tools are often complementary, each focusing on a distinct aspect of
numerical programming. Building reliable floating point applications
typically requires addressing several of these aspects, which makes easy
composition essential. This paper describes the composition of two recent
floating-point tools: Herbie, which performs accuracy optimization, and
Daisy, which performs accuracy verification. We find that the combination
provides numerous benefits to users, such as being able to use Daisy to check
whether Herbie's unsound optimizations improved the worst-case roundoff
error, as well as benefits to tool authors, including uncovering a number of
bugs in both tools. The combination also allowed us to compare the different
program rewriting techniques implemented by these tools for the first time.
The paper lays out a road map for combining other floating-point tools and
for surmounting common challenges.
</blockquote>
<h2>Paper</h2>
<p>
The paper uses the FPBench benchmarks and tooling to combine and
compare the Herbie and Diasy tools. The paper demonstrates the
importance of testing combinations of tools and describes some of
the challenges that had to be surmounted. It is available
in <a href="fm18-paper.pdf">PDF format</a>. All code described in
the paper is
also <a href="https://github.com/FPBench/FPBench/tree/daisy-herbie">freely
available online</a>.
</p>
</body>
</html>