Name
Abstract | ||
|---|---|---|
Floating-point arithmetic is widely used in scientific computing. While many programmers are subliminally aware that floating-point numbers only approximate the reals, few are cognizant of the dangers this entails for programming. Such dangers range from tolerable rounding errors in sequential programs, to unexpected, divergent control flow in parallel code. To address these problems, we present a decision procedure for floating-point arithmetic (FPA) that exploits the proximity to real arithmetic (RA), via a loss-less reduction from FPA to RA. Our procedure does not involve any form of bit-blasting or bit-vectorization, and can thus generate much smaller back-end decision problems, albeit in a more complex logic. This trade-off is beneficial for the exact and reliable analysis of parallel scientific software, which tends to give rise to large but benignly structured formulas. We have implemented a prototype decision engine and present encouraging results analyzing such software for numerical accuracy. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.7873/DATE.2014.130 | Design, Automation and Test in Europe Conference and Exhibition |
Keywords | Field | DocType |
floating point arithmetic,parallel programming,software tools,FPA,RA,back-end decision problems,bit blasting,bit vectorization,divergent control flow,floating point arithmetic,floating point reasoning,floating-point-to-real reduction,numerical accuracy,parallel code,parallel scientific software,prototype decision engine,real arithmetic,rounding errors,scientific computing,sequential programs,structured formulas | Computer science,Floating point,Floating-point unit,Arbitrary-precision arithmetic,Parallel computing,Double-precision floating-point format,Arithmetic logic unit,Arithmetic,Theoretical computer science,Machine epsilon,Binary scaling,Minifloat | Conference |
ISSN | Citations | PageRank |
1530-1591 | 7 | 0.54 |
References | Authors | |
6 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Miriam Leeser | 1 | 10 | 2.35 |
| Saoni Mukherjee | 2 | 7 | 0.54 |
| Jaideep Ramachandran | 3 | 7 | 0.87 |
| Thomas Wahl | 4 | 103 | 10.21 |