Conference proceeding
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
2015 IEEE 22nd Symposium on Computer Arithmetic, Vol.2015-, pp.160-167
06/2015
DOI: 10.1109/ARITH.2015.26
Abstract
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.
Details
- Title: Subtitle
- An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic
- Creators
- Martin Brain - University of OxfordCesare Tinelli - University of IowaPhilipp Ruemmer - Uppsala UniversityThomas Wahl - Northeastern University
- Resource Type
- Conference proceeding
- Publication Details
- 2015 IEEE 22nd Symposium on Computer Arithmetic, Vol.2015-, pp.160-167
- Publisher
- IEEE
- DOI
- 10.1109/ARITH.2015.26
- ISSN
- 1063-6889
- Language
- English
- Date published
- 06/2015
- Academic Unit
- Computer Science
- Record Identifier
- 9984259409202771
Metrics
39 Record Views