一种抽象引导的可扩展和严格浮点错误分析方法
An Abstraction-guided Approach to Scalable and Rigorous Floating-Point Error Analysis
摘要：
用于严格浮点舍入误差分析的自动化技术在包括正确性的形式化验证和精度调整的领域中是重要的。现有的工具和技术虽然提供了严格的边界，但无法分析具有数百个以上运算符的表达式，因此无法涵盖重要的实际问题。在这项工作中，我们提出了讽刺，一个新的工具，揭示了如何通过增量分析，抽象和明智地使用具体和象征性的评估相结合，可以实现可扩展性和边界紧密性。Satire已经处理了超过20万个操作员的问题。我们提出了讽刺的基本错误分析方法，信息理论抽象，和广泛的案例研究，与评估覆盖FFT，洛伦兹方程系统，和各种PDE模板类型。我们的研究结果表明讽刺的界限，其可接受的运行时间，并提供了宝贵的见解的紧密性。
英文摘要：
Automated techniques for rigorous floating-point round-off error analysis are important in areas including formal verification of correctness and precision tuning. Existing tools and techniques, while providing tight bounds, fail to analyze expressions with more than a few hundred operators, thus unable to cover important practical problems. In this work, we present Satire, a new tool that sheds light on how scalability and bound-tightness can be attained through a combination of incremental analysis, abstraction, and judicious use of concrete and symbolic evaluation. Satire has handled problems exceeding 200K operators. We present Satire's underlying error analysis approach, information-theoretic abstraction heuristics, and a wide range of case studies, with evaluation covering FFT, Lorenz system of equations, and various PDE stencil types. Our results demonstrate the tightness of Satire's bounds, its acceptable runtime, and valuable insights provided.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
