一句话：将生成高误差浮点输入建模为覆盖最大化问题，用符号执行实现工具 FPGen 并高效触发大误差。
浮点数常被用于模拟实数运算，但其舍入误差会在执行中传播和累积。生成能最大化数值误差的输入，对评估浮点代码的精度至关重要。本文把生成高误差浮点输入的问题形式化为代码覆盖最大化问题，并用符号执行求解。作者定义了不精度检查来检测较大的精度损失与抵消现象，并在程序中的关键位置注入这些检查，构造特殊分支；当输入覆盖这些分支时，结果很可能出现大误差。随后，论文应用符号执行生成能触发这些特殊分支的输入，并给出使方法实用的优化。作者实现了名为 FPGen 的工具，并在包含矩阵计算和统计库在内的 21 个数值程序上评估。结果表明，FPGen 能为其中 20 个程序暴露误差，且触发的误差平均比现有最优技术大两个数量级以上。
Floating point is widely used in software to emulate arithmetic over reals. Unfortunately, floating point leads to rounding errors that propagate and accumulate during execution. Generating inputs to maximize the numerical error is critical when evaluating the accuracy of floating-point code. In this paper, we formulate the problem of generating high error-inducing floating-point inputs as a code coverage maximization problem solved using symbolic execution. Specifically, we define inaccuracy checks to detect large precision loss and cancellation. We inject these checks at strategic program locations to construct specialized branches that, when covered by a given input, are likely to lead to large errors in the result. We apply symbolic execution to generate inputs that exercise these specialized branches, and describe optimizations that make our approach practical. We implement a tool named FPGen and present an evaluation on 21 numerical programs including matrix computation and statistics libraries. We show that FPGen exposes errors for 20 of these programs and triggers errors that are, on average, over 2 orders of magnitude larger than the state of the art.