City Research Online

Building Better Bit-Blasting for Floating-Point Problems

Brain, M. ORCID: 0000-0003-4216-7151, Schanda, F. and Sun, Y. (2019). Building Better Bit-Blasting for Floating-Point Problems. Paper presented at the International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2019, 6-7 April 2019, Prague, Czech Republic.

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.

Publication Type: Conference or Workshop Item (Paper)
Additional Information: The final authenticated version will be available online at http://www.springer.com/computer/lncs?SGWID=0-164-0-0-0
Publisher Keywords: IEEE-754, floating-point, satisfiability modulo theories, SMT
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Mathematics, Computer Science & Engineering > Computer Science
URI: http://openaccess.city.ac.uk/id/eprint/21921
[img]
Preview
Text - Accepted Version
Available under License Creative Commons: Attribution International Public License 4.0.

Download (384kB) | Preview

Export

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login