Hardware-Dependent Proofs of Numerical Programs

Hardware-Dependent Proofs of Numerical Programs
复制标题

数值程序的硬件相关证明

DOI：
--
复制
发表时间：
2011
期刊：
Certified Programs and Proofs
影响因子：
--
通讯作者：
Claude Marché
Claude Marché
中科院分区：
--
文献类型：
--
作者：
T. Nguyen;Claude Marché

文献摘要

被引文献

相似文献

我们提出了一种通过分析数值程序编译的汇编代码来证明其行为属性的方法。我们重点关注浮点计算中可能出现的问题和陷阱。对汇编代码的直接分析使我们能够考虑与体系结构或编译器相关的功能，例如扩展精度寄存器的可能使用。 该方法是在用于演绎验证的通用 Why 平台之上实现的，该平台允许我们进行实验，通过组合多个后端自动证明器来释放证明。
We present an approach for proving behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. The approach is implemented on top of the generic Why platform for deductive verification, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.