“Invertibility Conditions for Floating-Point Formulas” by Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 116-136. New York, New York.
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.
BibTeX entry:
@inproceedings{BNP+19,
author = {Martin Brain and Aina Niemetz and Mathias Preiner and Andrew
Reynolds and Clark Barrett and Cesare Tinelli},
editor = {Isil Dillig and Serdar Tasiran},
title = {Invertibility Conditions for Floating-Point Formulas},
booktitle = {Proceedings of the {\it 31^{st}} International Conference
on Computer Aided Verification (CAV '19)},
series = {Lecture Notes in Computer Science},
volume = {11561},
pages = {116--136},
publisher = {Springer International Publishing},
month = jul,
year = {2019},
isbn = {978-3-030-25542-8},
doi = {10.1007/978-3-030-25543-5_8},
note = {New York, New York},
url = {http://theory.stanford.edu/~barrett/pubs/BNP+19.pdf}
}
(This webpage was created with bibtex2web.)