FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Combining Tools for Optimization and Analysis of Floating-Point Computations

Authors: Heiko Becker, Pavel Panchekha, Eva Darulova and Zachary Tatlock

Paper Information

Title:Combining Tools for Optimization and Analysis of Floating-Point Computations
Authors:Heiko Becker, Pavel Panchekha, Eva Darulova and Zachary Tatlock
Proceedings:FM FMComplete
Editors: Jan Peleska, Klaus Havelund and Bill Roscoe
Keywords:floating-point optimization, floating-point analysis, roundoff error
Abstract:

ABSTRACT. Recent renewed interest in optimization and analysis of 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.

Pages:9
Talk:Jul 16 17:00 (Session 115B)
Paper: