验证浮点计算的陷阱
The pitfalls of verifying floating-point computations
AI总结：
针对关键系统中浮点计算验证的难题，本文通过具体示例揭示语义受编译器等因素影响的陷阱，并提出分析软件中的解决方案。
摘要：
当前关键系统普遍使用大量浮点计算，因此对包含浮点运算符的程序进行测试或静态分析已成为优先事项。然而，正确定义常见浮点实现的语义颇具挑战性，因为语义可能受源码级别之外的许多因素影响而变化，例如编译器所做的选择。我们在此给出可能出现问题的具体示例，以及可在分析软件中实施的解决方案。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
