FPScan：一种用于浮点异常检测的自动化基于约束的分析器
FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection
浏览论文内容
中文总结 AI 辅助
FPScan是一种基于约束的自动化分析工具，通过静态分析和SMT求解，检测浮点程序中的灾难性抵消与吸收异常，并在FPBench基准上验证了有效性。
中文摘要 AI 辅助
编写无错误的浮点程序是一项具有挑战性的任务，尤其是对于那些缺乏数值分析和舍入误差传播方面扎实背景的程序员而言。最先进的技术通常旨在通过静态或动态分析来限制此类误差。然而，只有少数工具明确处理关键的浮点陷阱，如吸收和灾难性抵消。这些异常代表了舍入误差被显著放大的情况，导致有限精度计算的语义与实数语义产生显著偏差。在本文中，我们提出了FPScan，一种新颖的工具，用于正式定义和检测浮点程序中的灾难性抵消和吸收。我们的方法首先基于抽象解释的自定义静态分析器来推断所有程序变量的数量级。然后利用该数量级信息构建一组一阶约束，用于建模程序中的误差传播和数值精度。最后，我们使用现成的SMT求解器来确定程序是否存在这些关键数值陷阱。我们在FPBench（一个知名的浮点程序基准测试套件）上进行了实验，以评估我们工具的有效性。我们还与最先进的工具在可靠性和分析时间方面进行了比较。
英文摘要
Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.
发表机构
- Fédération ENAC ISAE-SUPAERO ONERA, Université de Toulouse（ENAC ISAE-SUPAERO ONERA 联合会，图卢兹大学）
机构由 AI 辅助整理，请以论文原文为准。
