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

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: 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: http://dx.doi.org/10.1007/978-3-030-17462-0_5
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]
Preview
Text - Accepted Version
Available under License Creative Commons: Attribution International Public License 4.0.

Download (384kB) | Preview

Export

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

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login