An automatable formal semantics for IEEE-754 floating-point arithmetic
2015 (English)In: Proc. 22nd Symposium on Computer Arithmetic / [ed] Muller, JM; Tisserand, A; Villalba, J, IEEE Computer Society, 2015, 160-167 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
IEEE Computer Society, 2015. 160-167 p.
, Proceedings Symposium on Computer Arithmetic, ISSN 1063-6889
IdentifiersURN: urn:nbn:se:uu:diva-268740DOI: 10.1109/ARITH.2015.26ISI: 000380575000024ISBN: 9781479986637OAI: oai:DiVA.org:uu-268740DiVA: diva2:878815
ARITH 2015, June 22–24, Lyon, France
FunderSwedish Research Council, 2011-6310