Sciweavers

Share
ARITH
2015
IEEE

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

4 years 10 months ago
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.
Martin Brain, Cesare Tinelli, Philipp Rümmer,
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where ARITH
Authors Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
Comments (0)
books