Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
复制标题
使用自动定理证明器对超越定点和浮点算法进行形式验证
DOI：
10.1145/3543670
复制
发表时间：
2022
影响因子：
1
通讯作者：
Coward S
中科院分区：
文献类型：
--
作者：
Coward S
我们提出了一种用于形式化验证先验硬件和软件算法的方法，该方法可以扩展到更高的精度，而不会经历运行时间的指数增长。一类使用分段多项式近似来计算结果的实现使用MetiTarski来验证，MetiTarski是一个自动定理证明器，它为每次调用验证一系列输入。该方法被应用于Cadence Design Systems的商业实现，与穷举测试方法相比，运行时间有显著提高，并成功地证明了一个实现的预期精度过于乐观。在软件中复制正弦实现的验证，以前使用另一种定理证明技术，证明了MetiTarski方法是一个可行的竞争对手。平方根函数的52位实现的验证突出了该方法的高精度能力。
We present a method for formal verification of transcendental hardware and software algorithms that scales to higher precision without suffering an exponential growth in runtimes. A class of implementations using piecewise polynomial approximation to compute the result is verified using MetiTarski, an automated theorem prover, which verifies a range of inputs for each call. The method was applied to commercial implementations from Cadence Design Systems with significant runtime gains over exhaustive testing methods and was successful in proving that the expected accuracy of one implementation was overly optimistic. Reproducing the verification of a sine implementation in software, previously done using an alternative theorem-proving technique, demonstrates that the MetiTarski approach is a viable competitor. Verification of a 52-bit implementation of the square root function highlights the method’s high-precision capabilities.
登录
查看更多内容
影响因子：
3.7
作者：
M. Daumas;D. Lester;C. Muñoz
通讯作者：
C. Muñoz
DOI：
--
发表时间：
1999
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
J. Harrison
通讯作者：
J. Harrison
具有类似 LPO 性质的 Knuth-Bendix 排序的扩展
影响因子：
5
作者：
Michel Ludwig;Uwe Waldmann
通讯作者：
Uwe Waldmann
CR-LIBM：正确舍入的基本函数库
影响因子：
--
作者：
Catherine Daramy;D. Defour;F. de Dinechin;J. Muller
通讯作者：
J. Muller
用于改进 IA-64 上超越函数的新算法
DOI：
10.1109/arith.1999.762822
发表时间：
1999
期刊：
Proceedings 14th IEEE Symposium on Computer Arithmetic (Cat. No.99CB36336)
影响因子：
--
作者：
S. Story;P. T. P. Tang
通讯作者：
P. T. P. Tang