City Research Online

Invertibility Conditions for Floating-Point Formulae

Brain, M. ORCID: 0000-0003-4216-7151, Niemetz, A., Preiner, M., Reynolds, A., Barrett, C. and Tinelli, C. (2019). Invertibility Conditions for Floating-Point Formulae. In: 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 Mathematics, Computer Science & Engineering > Computer Science
URI: http://openaccess.city.ac.uk/id/eprint/22749
[img]
Preview
Text - Published Version
Available under License Creative Commons Attribution.

Download (783kB) | Preview

Export

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login