Building Better Bit-Blasting for Floating-Point Problems

Martin Brain, Florian Schanda, Youcheng Sun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

An effective approach to handling the theory of floating-point is to reduce it to the theory of bit-vectors. Implementing the required encodings is complex, error prone and requires a deep understanding of floating-point hardware. This paper presents SymFPU, a library of encodings that can be included in solvers. It also includes a verification argument for its correctness, and experimental results showing that its use in CVC4 out-performs all previous tools. As well as a significantly improved performance and correctness, it is hoped this will give a simple route to add support for the theory of floating-point.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
Pages79-98
Number of pages20
DOIs
Publication statusPublished - 4 Apr 2019

Fingerprint

Dive into the research topics of 'Building Better Bit-Blasting for Floating-Point Problems'. Together they form a unique fingerprint.

Cite this