Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL / Theorem proving - Abdel-Hamid, Amr T.; Akbarpour, Behzad; Harrison, John.; Tahar, Sofine