@inproceedings{4b07943a9b4641eca04d5e46a7f7e8a8,
title = "Building Better Bit-Blasting for Floating-Point Problems",
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.",
author = "Martin Brain and Florian Schanda and Youcheng Sun",
year = "2019",
month = apr,
day = "4",
doi = "10.1007/978-3-030-17462-0_5",
language = "English",
isbn = "9783030174613",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "79--98",
editor = "Tom{\'a}{\v s} Vojnar and Lijun Zhang",
booktitle = "Tools 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",
}