A Machine-Checked Theory of Floating Point Arithmetic

A Machine-Checked Theory of Floating Point Arithmetic
复制标题

机器检验的浮点运算理论

DOI：
--
复制
发表时间：
1999
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
通讯作者：
J. Harrison
J. Harrison
中科院分区：
--
文献类型：
--
作者：
J. Harrison

文献摘要

被引文献

相似文献

英特尔正在将形式验证应用于默塞德中使用的各种数学软件，Merced是新IA-64体系结构的第一个实现。本文讨论了一个通用浮点库的发展，给出了基本术语的定义，并包含重要引理的形式证明。我们还简要介绍了迄今为止如何在核查工作中使用这一方法。
Intel is applying formal Verification to various pieces of mathematical software used in Merced, the first implementation of the new IA-64 architecture. This paper discusses the development of a generic floating point library giving definitions of the fundamental terms and containing formal proofs of important lemmas. We also briefly describe how this has been used in the Verification effort so far.