paperbot · PL 论文追踪

全部论文 待读 收藏

P0 FPCC: Detecting Floating-Point Errors via Chain Conditions

FPCC:基于链条件检测浮点误差
OOPSLA 8(OOPSLA2)2024匹配度 8/10 · 该论文直接研究浮点程序分析中的误差触发输入检测问题,提出链条件并实现工具 FPCC,在 GSL 等基准上显著优于 ATOMU,符合用户对浮点程序分析、问题驱动和工具落地的兴趣;但未涉及 LLM/Agent 或贝叶斯程序分析交叉。引用 8 inbox
Xin Yi, Hengbiao Yu, Liqian Chen, Xiaoguang Mao, Ji Wang
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:提出链条件引导搜索触发浮点误差的输入,实现工具FPCC,显著优于ATOMU。

浮点运算的舍入误差会传播累积,导致不可接受的结果,检测能触发显著误差的输入对数值程序可靠性至关重要。现有方法依赖高精度计算的影子执行或存在假阳性。本文提出链条件来刻画浮点误差的传播与累积,并以此引导搜索触发误差的输入,实现了工具FPCC。在GNU科学库的88个函数及21个多输入函数上评估:FPCC报告的rank-1输入100%触发显著误差,而ATOMU仅72.69%;总体99.64%(1049/1053)的输入触发显著误差,ATOMU仅19.45%(141/723);检测速度提升2.17倍,且在多输入函数上优于现有技术。

问题
浮点舍入误差传播累积会导致数值程序结果不可靠,而现有触发误差输入生成方法依赖高精度影子执行或存在假阳性。
方法
提出链条件刻画浮点误差传播与累积,并以此引导搜索触发误差的输入,实现工具FPCC。
评估
在GSL的88个函数及21个多输入函数上评估,FPCC在触发显著误差的精度、速度和多输入支持上均优于ATOMU。
原文摘要(Abstract)

Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC .

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{YiYCM024,
  title = {FPCC: Detecting Floating-Point Errors via Chain Conditions},
  author = {Xin Yi and Hengbiao Yu and Liqian Chen and Xiaoguang Mao and Ji Wang},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689764}
}