一句话：提出 Magneto，用区间约束满足自动生成数值规约的测试与 oracle，检测浮点代码的精度、鲁棒性与功能缺陷。
变异测试可检验代码是否满足与实现无关的功能规约，并评估测试集充分性，但现有方法没有考虑浮点代码实现数值规约时出现的精度要求，而这在安全关键软件中很常见。本文提出 Magneto，一种面向实值数值规约的变异测试实例化方法，可全自动生成测试集，用于发现数值代码的精度、鲁棒性和功能行为缺陷。其核心是将测试用例与 oracle 生成形式化为区间域上的约束满足问题，从而可靠地界定误差，同时保持效率。作者在标准浮点基准集上评估 Magneto，发现其相比随机测试基线能更有效地生成有用的充分测试集。
Mutation testing is an established approach for checking whether code satisfies a code-independent functional specification, and for evaluating whether a test set is adequate. Current mutation testing approaches, however, do not account for accuracy requirements that appear with numerical specifications implemented in floating- point arithmetic code, but which are a frequent part of safety-critical software. We present Magneto, an instantiation of mutation testing that fully automatically generates a test set from a real-valued specification. The generated tests check numerical code for accuracy, robustness and functional behavior bugs. Our technique is based on formulating test case and oracle generation as a constraint satisfaction problem over interval domains, which soundly bounds errors, but is nonetheless efficient. We evaluate Magneto on a standard floating-point benchmark set and find that it outperforms a random testing baseline for producing useful adequate test sets.