
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Florent de Dinechin, Christoph Lauter, Guillaume Melquiond, "Certifying the FloatingPoint Implementation of an Elementary Function Using Gappa," IEEE Transactions on Computers, vol. 60, no. 2, pp. 242253, February, 2011.  
BibTex  x  
@article{ 10.1109/TC.2010.128, author = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond}, title = {Certifying the FloatingPoint Implementation of an Elementary Function Using Gappa}, journal ={IEEE Transactions on Computers}, volume = {60}, number = {2}, issn = {00189340}, year = {2011}, pages = {242253}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2010.128}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Certifying the FloatingPoint Implementation of an Elementary Function Using Gappa IS  2 SN  00189340 SP242 EP253 EPD  242253 A1  Florent de Dinechin, A1  Christoph Lauter, A1  Guillaume Melquiond, PY  2011 KW  Correctness proofs KW  error analysis KW  elementary function approximation. VL  60 JA  IEEE Transactions on Computers ER   
[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 FloatingPoint Arithmetic. Birkhäuser Boston, 2009.
[2] IEEE Standard for FloatingPoint Arithmetic, IEEE Standard 754, IEEE CS, 2008.
[3] D. Goldberg, "What Every Computer Scientist Should Know About FloatingPoint Arithmetic," ACM Computing Surveys, vol. 23, no. 1, pp. 547, 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. 410423, Sept. 1991.
[6] F. de Dinechin, A. Ershov, and N. Gast, "Towards the PostUltimate libm," Proc. 17th IEEE Symp. Computer Arithmetic, pp. 288295, June 2005.
[7] F. de Dinechin, C.Q. Lauter, and J.M. Muller, "Fast and Correctly Rounded Logarithms in DoublePrecision," Theoretical Informatics and Applications, vol. 41, pp. 85102, 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 ComputerAided Design (FMCAD '00), pp. 217233, 2000.
[10] T.J. Dekker, "A Floating Point Technique for Extending the Available Precision," Numerische Mathematik, vol. 18, no. 3, pp. 224242, 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 FloatingPoint Numbers and Its Application to Exact Computing," Proc. 14th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '01), pp. 169184, 2001.
[13] S. Gal, "Computing Elementary Functions: A New Approach for Achieving High Accuracy and Good Performance," Accurate Scientific Computations, pp. 116, 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 IA64," Proc. 14th IEEE Symp. Computer Arithmetic, pp. 411, Apr. 1999.
[16] R.C. Li, P. Markstein, J.P. Okada, and J.W. Thomas, "The Libm Library and FloatingPoint Arithmetic for HPUX on Itanium," technical report, HewlettPackard Company, Apr. 2001.
[17] J.M. Muller, Elementary Functions: Algorithms and Implementation, second ed. Birkhäuser, 2006.
[18] D. Priest, "Fast TableDriven Algorithms for Interval Elementary Functions," Proc. 13th IEEE Symp. Computer Arithmetic, pp. 168174, 1997.
[19] P. Markstein, IA6 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. 169176, 2009.
[21] S. Chevillard, J. Harrison, M. Joldeş, and C. Lauter, "Efficient and Accurate Computation of Upper Bounds of Approximation Errors," Technical Report RR 20102, LIP, CNRS/ENS Lyon/INRIA/Université de Lyon, INRIA, LORIA, CACAO Project and Intel Corporation, Jan. 2010.
[22] P.H. Sterbenz, FloatingPoint Computation. PrenticeHall, 1974.
[23] F. de Dinechin and S. Maidanov, "Software Techniques for Perfect Elementary Functions in FloatingPoint 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. 143153, 2003.
[25] W. Hofschuster and W. Krämer, "FI_LIB, eine Schnelle und Portable Funktionsbibliothek für Reelle Argumente und Reelle Intervalle im IEEEDoubleFormat," 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. 299324, 2006.
[27] M. Daumas and G. Melquiond, "Generating Formally Certified Bounds on Values and RoundOff Errors," Proc. Sixth Conf. Real Numbers and Computers, 2004.
[28] G. Melquiond and S. Pion, "Formally Certified FloatingPoint Filters for Homogeneous Geometric Predicates," Theoretical Informatics and Applications, vol. 41, no. 1, pp. 5770, 2007.
[29] S. Boutin, "Using Reflection to Build Efficient and Certified Decision Procedures," Proc. Third Int'l Symp. Theoretical Aspects of Computer Software, pp. 515529, 1997.
[30] G. Huet, G. Kahn, and C. PaulinMohring, The Coq Proof Assistant: A Tutorial, Version 8.0, ftp://ftp.inria.fr/INRIA/coq/current/doc 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. 188195, 2005.
[32] S. Owre, J.M. Rushby, and N. Shankar, "PVS: A Prototype Verification System," Proc. 11th Int'l Conf. Automated Deduction, pp. 748752, 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 RR200543, Laboratoire de l'Informatique du Parallélisme (LIP), INRIA, Sept. 2005.
[35] C.Q. Lauter and F. de Dinechin, "Optimising Polynomials for FloatingPoint Implementation" Proc. Eighth Conf. Real Numbers and Computers, pp. 716, July 2008.