We extend the Stainless deductive verifier with floating-point support, providing the first automated verification support for floating-point numbers for a subset of Scala that includes polymorphism, recursion and higher-order functions. We follow the recent approach in the KeY verifier to axiomatise reasoning about mathematical functions, but go further by supporting all functions from Scala's math API, and by verifying the correctness of the axioms against the actual implementation in Stainless itself. We validate Stainless' floating-point support on a new set of benchmarks sampled from real-world code from GitHub, showing that it can verify specifications about, e.g., ranges of output or absence of special values for most supported functions, or produce counter-examples when the specifications do not hold.

翻译：我们扩展了Stainless演绎验证器以支持浮点数，为包含多态、递归和高阶函数的Scala子集首次提供了浮点数的自动化验证支持。我们遵循KeY验证器中近期提出的数学函数公理化推理方法，但进一步支持了Scala数学API中的所有函数，并通过在Stainless自身中验证公理相对于实际实现的正确性来强化该方法。我们在从GitHub真实代码中采样的新基准测试集上验证了Stainless的浮点支持功能，结果表明其能够验证大多数受支持函数的输出范围或特殊值缺失等规范，或在规范不成立时生成反例。