Invertibility Conditions for Floating-Point Formulas

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:

   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 = {}

(This webpage was created with bibtex2web.)