
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Sylvie Boldo, Marc Daumas, RenCang Li, "Formally Verified Argument Reduction with a Fused MultiplyAdd," IEEE Transactions on Computers, vol. 58, no. 8, pp. 11391145, August, 2009.  
BibTex  x  
@article{ 10.1109/TC.2008.216, author = {Sylvie Boldo and Marc Daumas and RenCang Li}, title = {Formally Verified Argument Reduction with a Fused MultiplyAdd}, journal ={IEEE Transactions on Computers}, volume = {58}, number = {8}, issn = {00189340}, year = {2009}, pages = {11391145}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2008.216}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Formally Verified Argument Reduction with a Fused MultiplyAdd IS  8 SN  00189340 SP1139 EP1145 EPD  11391145 A1  Sylvie Boldo, A1  Marc Daumas, A1  RenCang Li, PY  2009 KW  Argument reduction KW  fma KW  formal proof KW  Coq. VL  58 JA  IEEE Transactions on Computers ER   
[1] P. Markstein, IA64 and Elementary Functions: Speed and Precision. Prentice Hall, 2000.
[2] N. Brisebarre, D. Defour, P. Kornerup, J.M. Muller, and N. Revol, “A New RangeReduction Algorithm,” IEEE Trans. Computers, vol. 54, no. 3, pp. 331339, Mar. 2005.
[3] J.M. Muller, Elementary Functions, Algorithms and Implementation. Birkhauser, http://www.springer.com/west/home/birkhauser computer+ science?SGWID=44035322723779860 , 2006.
[4] R.C. Li, “Near Optimality of Chebyshev Interpolation for Elementary Function Computations,” IEEE Trans. Computers, vol. 53, no. 6, pp. 678687, June 2004.
[5] W.J. Cody and W. Waite, Software Manual for Elementary Functions. Prentice Hall, 1980.
[6] P.W. Markstein, “Computation of Elementary Functions on the IBM RISC System/6000 Processor,” IBM J. Research and Development, vol. 34, no. 1, pp.111119, http://www.research.ibm.com/journal/rd/341 ibmrd3401N.pdf, 1990.
[7] S. Story and P.T.P. Tang, “New Algorithms for Improved Transcendental Function on IA64,” Proc. 14th IEEE Symp. Computer Arithmetic (ARITH'99), I. Koren and P. Kornerup, eds., pp. 411, http://computer.org/proceedings/arith/0116 0116toc.htm, 1999.
[8] R.C. Li, S. Boldo, and M. Daumas, “Theorems on Efficient Argument Reductions,” Proc. 16th IEEE Symp. Computer Arithmetic (ARITH '03), J.C.Bajard and M. Schulte, eds., pp. 129136, http://hal.archives ouvertes.frhal00156244 , 2003.
[9] W. Kahan, Minimizing $q \times m  n$ , http://www.cs.berkeley.edu/~wkahan/testpi nearpi.c, 1983.
[10] J. Harrison, “A MachineChecked Theory of Floating Point Arithmetic,” Proc. 12th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '99), Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, eds., pp.113130, http://www.cl.cam.ac.uk/users/jrh/papers fparith.ps.gz, 1999.
[11] J. Harrison, “Formal Verification of Floating Point Trigonometric Functions,” Proc. Third Int'l Conf. Formal Methods in ComputerAided Design (FMCAD '00), W.A. Hunt and S.D. Johnson, eds., pp. 217233, 2000.
[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, http://hal.archivesouvertes.frhal00157285 , 2001.
[13] Y. Bertot and P. Castéran, “Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions,” Texts in Theoretical Computer Science. Springer, 2004.
[14] V.A. Carreño and P.S. Miner, “Specification of the IEEE854 FloatingPoint Standard in HOL and PVS,” Proc. 1995 Int'l Workshop Higher Order Logic Theorem Proving and Its Applications, http://shemesh.larc.nasa.gov/fm/ftp/larc/ vachug95.ps, 1995.
[15] D.M. Russinoff, “A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMDK7 Processor,” LMS J. Computation and Math., vol. 1, pp. 148200, http://www.onr.com/user/russ/davidk7divsqrt.ps , 1998.
[16] J. Harrison, “Floating Point Verification in HOL Light: The Exponential Function,” Technical Report 428, Univ. of Cambridge Computer Laboratory, http://www.cl.cam.ac.uk/users/jrh/papers tang.ps.gz, 1997.
[17] P.H. Sterbenz, Floating Point Computation. Prentice Hall, 1974.
[18] D. Goldberg, “What Every Computer Scientist Should Know about Floating Point Arithmetic,” ACM Computing Surveys, vol. 23, no. 1, pp. 547, http://doi.acm.org/10.1145103162.103163, 1991.
[19] S. Boldo and M. Daumas, “Properties of Two's Complement Floating Point Notations,” Int'l J. Software Tools for Technology Transfer, vol. 5, nos. 2/3, pp.237246, http://hal.archivesouvertes.frhal00157268 , 2004.
[20] D. Stevenson et al., “An American National Standard: IEEE Standard for Binary Floating Point Arithmetic,” ACM SIGPLAN Notices, vol. 22, no. 2, pp. 925, 1987.
[21] W.J. Cody, R. Karpinski et al., “A Proposed Radix and WordLength Independent Standard for Floating Point Arithmetic,” IEEE Micro, vol. 4, no. 4, pp. 86100, 1984.
[22] Pentium Pro Family: Developer's Manual, Programmer's Reference Manual, Intel, ftp://download.intel.com/design/pro/manuals 24269101.pdf, 1996.
[23] K.C. Ng, Argument Reduction for Huge Arguments: Good to the Last Bit, work in progress, http://www.validgh.comarg.ps, 1992.
[24] S. Boldo and J.M. Muller, “Some Functions Computable with a FusedMAC,” Proc. 17th IEEE Symp. Computer Arithmetic (ARITH '05), P. Montuschi and E. Schwarz, eds., pp. 5258, http://csdl.computer. org/comp/proceedings arith/, 2005.
[25] A.H. Karp and P. Markstein, “HighPrecision Division and Square Root,” ACM Trans. Math. Software, vol. 23, no. 4, pp. 561589, Dec. 1997.
[26] J.F. Reiser and D.E. Knuth, “Evading the Drift in Floating Point Addition,” Information Processing Letters, vol. 3, no. 3, pp. 8487, 1975.