Verifying bit-manipulations of floating-point
Abstract
Reasoning about floating-point is difficult and becomes only more so if there is an interplay between floating-point and bit-level operations. Even though real-world floating-point libraries use implementations that have such mixed computations, no systematic technique to verify the correctness of the implementations of such computations is known. In this paper, we present the first general technique for verifying the correctness of mixed binaries, which combines abstraction, analytical optimization, and testing. The technique provides a method to compute an error bound of a given implementation with respect to its mathematical specification. We apply our technique to Intel's implementations of transcendental functions and prove formal error bounds for these widely used routines.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 02, 2016
- Source ID
- 10.1145/2980983.2908107
Entities
People
- Alex Aiken
- Rahul Sharma
- Wonyeol Lee
Organizations
- Air Force Research Laboratory
- National Science Foundation
- Stanford University