Invertibility Conditions for Floating-Point Formulae

Brain, M. ORCID: 0000-0003-4216-7151, Niemetz, A., Preiner, M. , Reynolds, A., Barrett, C. & Tinelli, C. (2019). Invertibility Conditions for Floating-Point Formulae. In: Dillig, I. & Tasiran, S. (Eds.), Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, 11562. (pp. 116-136). Cham: Springer. ISBN 978-3-030-25542-8

Abstract

Automated reasoning procedures are essential for a number of applications that involve bit-exact floating-point computations. This paper presents conditions that characterize when a variable in a floating-point constraint has a solution, which we call invertibility conditions. We describe a novel workflow that combines human interaction and a syntax-guided synthesis (SyGuS) solver that was used for discovering these conditions. We verify our conditions for several floating-point formats. One implication of this result is that a fragment of floating-point arithmetic admits compact quantifier elimination. We implement our invertibility conditions in a prototype extension of our solver CVC4, showing their usefulness for solving quantified constraints over floating-points.

Publication Type:	Conference or Workshop Item (Paper)
Additional Information:	© The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
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