Automated reasoning tools often provide little or no support to reason
accurately and efficiently about floating-point arithmetic. As a
consequence, software verification systems that use these tools are
unable to reason reliably about programs containing floating-point
calculations or may give unsound results. These deficiencies are in
stark contrast to the increasing awareness that the improper use of
floating-point arithmetic in programs can lead to unintuitive and
harmful defects in software. To promote coordinated efforts towards
building efficient and accurate floating-point reasoning engines, this
paper presents a formalization of the IEEE-754 standard for
floating-point arithmetic as a theory in many-sorted first-order
logic. Benefits include a standardized syntax and unambiguous
semantics, allowing tool interoperability and sharing of benchmarks,
and providing a basis for automated, formal analysis of programs that
process floating-point data.