This Article 
 Bibliographic References 
 Add to: 
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
February 2011 (vol. 60 no. 2)
pp. 242-253
Florent de Dinechin, Université de Lyon, Lyon
Christoph Lauter, Intel Corporation, Hillsboro
Guillaume Melquiond, INRIA, Orsay
High confidence in floating-point programs requires proving numerical properties of final and intermediate values. One may need to guarantee that a value stays within some range, or that the error relative to some ideal value is well bounded. This certification may require a time-consuming proof for each line of code, and it is usually broken by the smallest change to the code, e.g., for maintenance or optimization purpose. Certifying floating-point programs by hand is, therefore, very tedious and error-prone. The Gappa proof assistant is designed to make this task both easier and more secure, due to the following novel features: It automates the evaluation and propagation of rounding errors using interval arithmetic. Its input format is very close to the actual code to validate. It can be used incrementally to prove complex mathematical properties pertaining to the code. It generates a formal proof of the results, which can be checked independently by a lower level proof assistant like Coq. Yet it does not require any specific knowledge about automatic theorem proving, and thus, is accessible to a wide community. This paper demonstrates the practical use of this tool for a widely used class of floating-point programs: implementations of elementary functions in a mathematical library.

[1] J.-M. Muller, N. Brisebarre, F. de Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, N. Revol, D. Stehlé, and S. Torres, Handbook of Floating-Point Arithmetic. Birkhäuser Boston, 2009.
[2] IEEE Standard for Floating-Point Arithmetic, IEEE Standard 754, IEEE CS, 2008.
[3] D. Goldberg, "What Every Computer Scientist Should Know About Floating-Point Arithmetic," ACM Computing Surveys, vol. 23, no. 1, pp. 5-47, Mar. 1991.
[4] R.E. Moore, Interval Analysis. Prentice Hall, 1966.
[5] A. Ziv, "Fast Evaluation of Elementary Mathematical Functions with Correctly Rounded Last Bit," ACM Trans. Math. Software, vol. 17, no. 3, pp. 410-423, Sept. 1991.
[6] F. de Dinechin, A. Ershov, and N. Gast, "Towards the Post-Ultimate libm," Proc. 17th IEEE Symp. Computer Arithmetic, pp. 288-295, June 2005.
[7] F. de Dinechin, C.Q. Lauter, and J.-M. Muller, "Fast and Correctly Rounded Logarithms in Double-Precision," Theoretical Informatics and Applications, vol. 41, pp. 85-102, 2007.
[8] J. Harrison, "Floating Point Verification in HOL Light: The Exponential Function," Technical Report 428, Univ. of Cambridge Computer Laboratory, 1997.
[9] J. Harrison, "Formal Verification of Floating Point Trigonometric Functions," Proc. Third Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '00), pp. 217-233, 2000.
[10] T.J. Dekker, "A Floating Point Technique for Extending the Available Precision," Numerische Mathematik, vol. 18, no. 3, pp. 224-242, 1971.
[11] D. Knuth, The Art of Computer Programming, Volume 2: Seminumerical Algorithms, third ed. Addison Wesley, 1997.
[12] M. Daumas, L. Rideau, and L. Théry, "A Generic Library of Floating-Point Numbers and Its Application to Exact Computing," Proc. 14th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '01), pp. 169-184, 2001.
[13] S. Gal, "Computing Elementary Functions: A New Approach for Achieving High Accuracy and Good Performance," Accurate Scientific Computations, pp. 1-16, Springer, 1986.
[14] P.T.P. Tang, "Table Lookup Algorithms for Elementary Functions and Their Error Analysis," Proc. 10th IEEE Symp. Computer Arithmetic, June 1991.
[15] S. Story and P. Tang, "New Algorithms for Improved Transcendental Functions on IA-64," Proc. 14th IEEE Symp. Computer Arithmetic, pp. 4-11, Apr. 1999.
[16] R.-C. Li, P. Markstein, J.P. Okada, and J.W. Thomas, "The Libm Library and Floating-Point Arithmetic for HP-UX on Itanium," technical report, Hewlett-Packard Company, Apr. 2001.
[17] J.-M. Muller, Elementary Functions: Algorithms and Implementation, second ed. Birkhäuser, 2006.
[18] D. Priest, "Fast Table-Driven Algorithms for Interval Elementary Functions," Proc. 13th IEEE Symp. Computer Arithmetic, pp. 168-174, 1997.
[19] P. Markstein, IA-6 and Elementary Functions Speed and Precision. Prentice Hall, 2000.
[20] S. Chevillard, C. Lauter, and M. Joldeş, "Certified and Fast Supremum Norms of Approximation Errors," Proc. 19th IEEE Symp. Computer Arithmetic, pp. 169-176, 2009.
[21] S. Chevillard, J. Harrison, M. Joldeş, and C. Lauter, "Efficient and Accurate Computation of Upper Bounds of Approximation Errors," Technical Report RR 2010-2, LIP, CNRS/ENS Lyon/INRIA/Université de Lyon, INRIA, LORIA, CACAO Project and Intel Corporation, Jan. 2010.
[22] P.H. Sterbenz, Floating-Point Computation. Prentice-Hall, 1974.
[23] F. de Dinechin and S. Maidanov, "Software Techniques for Perfect Elementary Functions in Floating-Point Interval Arithmetic," Proc. Seventh Conf. Real Numbers and Computers, July 2006.
[24] J. Harrison, "Formal Verification of Square Root Algorithms," Formal Methods in Systems Design, vol. 22, pp. 143-153, 2003.
[25] W. Hofschuster and W. Krämer, "FI_LIB, eine Schnelle und Portable Funktionsbibliothek für Reelle Argumente und Reelle Intervalle im IEEE-Double-Format," Technical Report 98/7, Institut für Wissenschaftliches Rechnen und Mathematische Modellbildung, Universität Karlsruhe, 1998.
[26] M. Lerch, G. Tischler, J.W. von Gudenberg, W. Hofschuster, and W. Krämer, "FILIB++, a Fast Interval Library Supporting Containment Computations," Trans. Math. Software, vol. 32, no. 2, pp. 299-324, 2006.
[27] M. Daumas and G. Melquiond, "Generating Formally Certified Bounds on Values and Round-Off Errors," Proc. Sixth Conf. Real Numbers and Computers, 2004.
[28] G. Melquiond and S. Pion, "Formally Certified Floating-Point Filters for Homogeneous Geometric Predicates," Theoretical Informatics and Applications, vol. 41, no. 1, pp. 57-70, 2007.
[29] S. Boutin, "Using Reflection to Build Efficient and Certified Decision Procedures," Proc. Third Int'l Symp. Theoretical Aspects of Computer Software, pp. 515-529, 1997.
[30] G. Huet, G. Kahn, and C. Paulin-Mohring, The Coq Proof Assistant: A Tutorial, Version 8.0, Tutorial.pdf.gz, 2004.
[31] M. Daumas, G. Melquiond, and C. Muñoz, "Guaranteed Proofs Using Interval Arithmetic," Proc. 17th IEEE Symp. Computer Arithmetic, pp. 188-195, 2005.
[32] S. Owre, J.M. Rushby, and N. Shankar, "PVS: A Prototype Verification System," Proc. 11th Int'l Conf. Automated Deduction, pp. 748-752, 1992.
[33] Int'l Standard ISO/IEC 9899:1999(E). Programming Languages—C, ISO/IEC, 1999.
[34] F. de Dinechin, C.Q. Lauter, and G. Melquiond, "Assisted Verification of Elementary Functions," Technical Report RR2005-43, Laboratoire de l'Informatique du Parallélisme (LIP), INRIA, Sept. 2005.
[35] C.Q. Lauter and F. de Dinechin, "Optimising Polynomials for Floating-Point Implementation" Proc. Eighth Conf. Real Numbers and Computers, pp. 7-16, July 2008.

Index Terms:
Correctness proofs, error analysis, elementary function approximation.
Florent de Dinechin, Christoph Lauter, Guillaume Melquiond, "Certifying the Floating-Point Implementation of an Elementary Function Using Gappa," IEEE Transactions on Computers, vol. 60, no. 2, pp. 242-253, Feb. 2011, doi:10.1109/TC.2010.128
Usage of this product signifies your acceptance of the Terms of Use.