HackerPapers

arXiv:cs/0701192cs.PL

The pitfalls of verifying floating-point computations

David Monniaux

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.

arXiv comments
Journal reference
ACM Transactions on Programming Languages and Systems 30, 3 (2008) 12
DOI
doi:10.1145/1353445.1353446
Subjects
cs.PLProgramming Languages math.NANumerical Analysis

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Mar 2014 to Mar 2014.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Why doesn't GCC optimize a*a*a*a*a*a to (a*a*a)*(a*a*a)? (2013) 1 comment

    • In the case of C compilers, they get floating-point right by re-defining what the language definition means: http://arxiv.org/abs/cs/0701192 There has been some progress since the time this report was an accurate description of the situation, but the situation is still mostly…

      pascal_cuoqView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.