Building Better Bit-Blasting for Floating-Point Problems

Martin Brain; Florian Schanda; Youcheng Sun

doi:10.1007/978-3-030-17462-0_5

Building Better Bit-Blasting for Floating-Point Problems

Martin Brain, Florian Schanda, Youcheng Sun

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

185 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 language	English
Title of host publication	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
Editors	Tomáš Vojnar, Lijun Zhang
Pages	79-98
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-030-17462-0_5
Publication status	Early online date - 04 Apr 2019
Externally published	Yes

Publication series

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

Access to Document

10.1007/978-3-030-17462-0_5Licence: CC BY

Building Better Bit-Blasting for Floating-Point Problems
Copyright 2019 the authors. This is an open access article published under a Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution and reproduction in any medium, provided the author and source are cited.
Accepted author manuscript, 457 KBLicence: CC BY

Cite this

Brain, M., Schanda, F., & Sun, Y. (2019). Building Better Bit-Blasting for Floating-Point Problems. In T. Vojnar, & L. Zhang (Eds.), 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 (pp. 79-98). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS). https://doi.org/10.1007/978-3-030-17462-0_5

Brain, Martin ; Schanda, Florian ; Sun, Youcheng. / Building Better Bit-Blasting for Floating-Point Problems. 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. editor / Tomáš Vojnar ; Lijun Zhang. 2019. pp. 79-98 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Brain, M, Schanda, F & Sun, Y 2019, Building Better Bit-Blasting for Floating-Point Problems. in T Vojnar & L Zhang (eds), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11427 LNCS, pp. 79-98. https://doi.org/10.1007/978-3-030-17462-0_5

Building Better Bit-Blasting for Floating-Point Problems. / Brain, Martin; Schanda, Florian; Sun, Youcheng.

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. ed. / Tomáš Vojnar; Lijun Zhang. 2019. p. 79-98 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Building Better Bit-Blasting for Floating-Point Problems

AU - Brain, Martin

AU - Schanda, Florian

AU - Sun, Youcheng

PY - 2019/4/4

Y1 - 2019/4/4

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

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

U2 - 10.1007/978-3-030-17462-0_5

DO - 10.1007/978-3-030-17462-0_5

M3 - Conference contribution

SN - 9783030174613

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 79

EP - 98

BT - 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

A2 - Vojnar, Tomáš

A2 - Zhang, Lijun

ER -

Brain M, Schanda F, Sun Y. Building Better Bit-Blasting for Floating-Point Problems. In Vojnar T, Zhang L, editors, 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. 2019. p. 79-98. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-17462-0_5

Building Better Bit-Blasting for Floating-Point Problems

Abstract

Publication series

Access to Document

Fingerprint

Cite this