Proving Floating-Point Numerical Programs by Analysis of their Assembly Code

Proving Floating-Point Numerical Programs by Analysis of their Assembly Code
复制标题

通过分析汇编代码来证明浮点数值程序

DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
C. Marché
C. Marché
中科院分区：
--
文献类型：
--
作者：
Nguyen Thi Mong Tuyen;C. 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 to accurately 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.