M. Aharoni, S. Asaf, R. Maharik, I. Nehama, I. Nikulshin, A. Ziv, "Solving Constraints on the Invisible Bits of the Intermediate Result for Floating-Point Verification", Proceedings of the 17th IEEE Symposium on Computer Arithmetic, Cape Cod, Massachusetts, June 27-29, 2005