论文标题
通过非线性真实掠夺者对浮点程序进行自动验证
Auto-active Verification of Floating-point Programs via Nonlinear Real Provers
论文作者
论文摘要
我们提供了一个程序，以根据其功能规范验证数值程序。我们的实现能够自动验证程序，以防止具有常见基本功能的严格错误范围。我们在几个示例上演示和评估了我们的实现，从而产生了正弦和平方根函数的第一个完全验证的火花实现。该过程使用一系列的转换和推导来集成现有的工具，这是基于Spark中的证明过程，其中3为什么会产生验证条件（VC）和SMT求解器之类的工具试图验证它们。我们添加针对VC的步骤，该步骤包含具有浮点操作和精确实际功能的不平等现象。 PROPAFP是我们对这些步骤的开源实施。这些步骤包括符号简化，通过间隔算术得出边界，并使用精确操作安全地替换浮点操作，并利用诸如Fptaylor或Gappa之类的工具来绑定表达式的复合圆形误差。最后，VC将其传递给了DREAL，METITARSKI或LPPAVER等掠夺者，这些抛弃者试图完成证明或建议可能的反例。
We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps. The steps include symbolic simplifications, deriving bounds via interval arithmetic, and safely replacing floating-point operations with exact operations, utilizing tools such as FPTaylor or Gappa to bound the compound rounding errors of expressions. Finally, the VCs are passed to provers such as dReal, MetiTarski or LPPaver which attempt to complete the proof or suggest possible counter-examples.
