City Research Online

Building Better Bit-Blasting for Floating-Point Problems

Brain, M. ORCID: 0000-0003-4216-7151, Schanda, F. & Sun, Y. (2019). Building Better Bit-Blasting for Floating-Point Problems. Tools and Algorithms for the Construction and Analysis of Systems, 11427, pp. 79-98. doi: 10.1007/978-3-030-17462-0_5


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.

Publication Type: Article
Additional Information: This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science. The final authenticated version is available online at:
Publisher Keywords: IEEE-754, floating-point, satisfiability modulo theories, SMT
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Science & Technology > Computer Science
School of Science & Technology > Computer Science > Software Reliability
[thumbnail of brain_schanda_tacas2019_extended.pdf]
Text - Accepted Version
Available under License Creative Commons: Attribution International Public License 4.0.

Download (384kB) | Preview


Add to AnyAdd to TwitterAdd to FacebookAdd to LinkedinAdd to PinterestAdd to Email


Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login