An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic

—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 floating-point reasoning engines, this paper presents a formalisation of the IEEE-754 standard for floating-point arithmetic as a theory in many-sorted first-order logic. Benefits include a standardised syntax and unambiguous semantics, allowing tool interoperability and sharing of benchmarks, and providing a basis for automated, formal analysis of programs using floating-point data.

• Type: Journal
• Year: 2015
• Where: ARITH
• Authors: Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
• Keywords: Applied Computing, ARITH 2015