A Formal Model of IEEE Floating Point Arithmetic

Lei Yu 📧 with contributions from Fabian Hellauer 📧, Fabian Immler 🌐 and Tjark Weber 📧

July 27, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This development provides a formal model of IEEE-754 floating-point 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.

License

BSD License

History

May 22, 2023
Added a model of floating-point arithmetic with a single NaN value.
Added a translation of floating-point arithmetic into SMT-LIB.
May 10, 2023
Added the IEEE rounding mode "roundNearestTiesToAway".
February 5, 2018
'Modernized' representation following the formalization in HOL4: former "float_format" and predicate "is_valid" is now encoded in a type "('e, 'f) float" where 'e and 'f encode the size of exponent and fraction.
September 25, 2017
Added conversions from and to software floating point numbers (by Fabian Hellauer and Fabian Immler).

Topics

Session IEEE_Floating_Point

Depends on

Used by

Cite

× 
@article{IEEE_Floating_Point-AFP,
  author  = {Lei Yu},
  title   = {A Formal Model of IEEE Floating Point Arithmetic},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2013},
  note    = {\url{https://isa-afp.org/entries/IEEE_Floating_Point.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: