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 |
Available under License Creative Commons: Attribution International Public License 4.0.
Download (384kB) | Preview
Export
Downloads
Downloads per month over past year
Metadata
MetadataActions (login required)
Admin Login