### 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

- Computer science/Data structures

### Session IEEE_Floating_Point

- IEEE
- IEEE_Properties
- FP64
- Conversion_IEEE_Float
- Double
- IEEE_Single_NaN
- IEEE_Single_NaN_SMTLIB

### Depends on

- Finite Machine Word Library

### Used by

- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
- CakeML

## Cite

×

IEEE_Floating_Point-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Jul 28, 2013 : Isabelle2013