A Formal Model of IEEE Floating Point Arithmetic
A Formal Model of IEEE Floating Point Arithmetic
复制标题
IEEE浮点运算的形式化模型
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Lei Yu
中科院分区：
文献类型：
--
作者：
Lei Yu
This development provides a formal model of IEEE-754 floatingpoint arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages. The definitions of the IEEE standard in Isabelle is ported from HOL Light [1].
