Conference item icon

Conference item

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 improv...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's Version

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-030-17462-0_5

Authors


More by this author
Institution:
University of Oxford
Schanda, F More by this author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Publisher:
Springer Publisher's website
Pages:
vol 11427
Series:
Lecture Notes in Computer Science
Publication date:
2019-04-04
Acceptance date:
2019-01-26
DOI:
EISBN:
978-3-030-17462-0
Pubs id:
pubs:985752
URN:
uri:605b2822-0e13-4400-a374-aab6df296ea3
UUID:
uuid:605b2822-0e13-4400-a374-aab6df296ea3
Local pid:
pubs:985752
ISBN:
978-3-030-17461-3

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP