Building Better Bit-Blasting for Floating-Point Problems

Martin Brain, Florian Schanda, Youcheng Sun

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)
43 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationTools 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
EditorsTomáš Vojnar, Lijun Zhang
Pages79-98
Number of pages20
DOIs
Publication statusEarly online date - 04 Apr 2019
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11427 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Building Better Bit-Blasting for Floating-Point Problems'. Together they form a unique fingerprint.

Cite this