The pitfalls of verifying floating-point computations
The pitfalls of verifying floating-point computations
复制标题
DOI：
10.1145/1353445.1353446
复制
发表时间：
2008-05-01
影响因子：
1.3
通讯作者：
Monniaux, David
中科院分区：
文献类型：
--
作者：
Monniaux, David
当前的关键系统经常使用大量的浮点计算，因此对包含浮点运算符的程序进行测试或静态分析已成为当务之急。然而，正确定义浮点的常见实现的语义是很棘手的，因为语义可能会根据源代码级别之外的许多因素而改变，例如编译器所做的选择。我们在这里给出了可能出现的问题的具体示例以及在分析软件中实施的解决方案。
Current critical systems often 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 according to many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions for implementing in analysis software.