用于Coq和HOL4中有限精度误差界的已验证证书检查器
编程语言
2018-08-24 v2
摘要
能够可靠地估计有限精度计算的舍入误差对于嵌入式系统和科学计算中的许多应用十分重要。由于连续实数与离散有限精度值之间的差异，自动化静态分析工具对于估计舍入误差极具价值。然而，结果的正确性仅与静态分析工具的实现相当。本文提出一个形式化验证的模块化工具，其全自动检查编码在证书中的有限精度舍入误差界的正确性。我们给出了针对Coq和HOL4的证书生成与检查的两种实现，并在文献中的若干例子上进行了评估。实验同时使用了Coq和HOL4的逻辑内评估，以及逻辑外提取代码的执行：我们对Coq提取的未验证OCaml代码和CakeML生成的已验证二进制文件进行了基准测试。
引用
@article{arxiv.1707.02115,
title = {A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4},
author = {Heiko Becker and Nikita Zyuzin and Raphael Monat and Eva Darulova and Magnus O. Myreen and Anthony Fox},
journal= {arXiv preprint arXiv:1707.02115},
year = {2018}
}