Building Better Bit-Blasting for Floating-Point Problems

Martin Brain, Florian Schanda, Youcheng Sun

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)
185 Downloads (Pure)


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
EditorsTomáš Vojnar, Lijun Zhang
Number of pages20
Publication statusEarly online date - 04 Apr 2019
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11427 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


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

Cite this