
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Sylvie Boldo, Guillaume Melquiond, "Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd," IEEE Transactions on Computers, vol. 57, no. 4, pp. 462471, April, 2008.  
BibTex  x  
@article{ 10.1109/TC.2007.70819, author = {Sylvie Boldo and Guillaume Melquiond}, title = {Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd}, journal ={IEEE Transactions on Computers}, volume = {57}, number = {4}, issn = {00189340}, year = {2008}, pages = {462471}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2007.70819}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd IS  4 SN  00189340 SP462 EP471 EPD  462471 A1  Sylvie Boldo, A1  Guillaume Melquiond, PY  2008 KW  Computer arithmetic KW  Verification VL  57 JA  IEEE Transactions on Computers ER   
[1] D. Stevenson et al., “A Proposed Standard for Binary Floating Point Arithmetic,” Computer, vol. 14, no. 3, pp. 5162, Mar. 1981.
[2] D. Stevenson et al., “An American National Standard: IEEE Standard for Binary FloatingPoint Arithmetic,” ACM SIGPLAN Notices, vol. 22, no. 2, pp. 925, 1987.
[3] G. Melquiond and S. Pion, “Formally Certified FloatingPoint Filters for Homogeneous Geometric Predicates,” Theoretical Informatics and Applications, vol. 41, no. 1, pp. 5770, 2007.
[4] S.A. Figueroa, “When Is Double Rounding Innocuous,” SIGNUM Newsletter, vol. 30, no. 3, pp. 2126, 1995.
[5] J. von Neumann, “First Draft of a Report on the EDVAC,” IEEE Annals of the History of Computing, vol. 15, no. 4, pp. 2775, 1993.
[6] D. Goldberg, “What Every Computer Scientist Should Know about FloatingPoint Arithmetic,” ACM Computing Surveys, vol. 23, no. 1, pp. 547, 1991.
[7] M.D. Ercegovac and T. Lang, Digital Arithmetic. Morgan Kaufmann, 2004.
[8] C. Lee, “Multistep Gradual Rounding,” IEEE Trans. Computers, vol. 38, no. 4, pp. 595600, Apr. 1989.
[9] 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, pp.169184, 2001.
[10] Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag, 2004.
[11] S. Boldo, “Preuves Formelles en Arithmétiques à Virgule Flottante,” PhD dissertation, École Normale Supérieure de Lyon, Nov. 2004.
[12] S. Boldo and G. Melquiond, “When Double Rounding Is Odd,” Proc. 17th IMACS World Congress Computational and Applied Math., 2005.
[13] T.J. Dekker, “A FloatingPoint Technique for Extending the Available Precision,” Numerische Mathematik, vol. 18, no. 3, pp.224242, 1971.
[14] D.E. Knuth, The Art of Computer Programming: Seminumerical Algorithms, vol. 2. Addison Wesley, 1969.
[15] S. Boldo, “Pitfalls of a Full FloatingPoint Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms,” Proc. Third Int'l Joint Conf. Automated Reasoning, 2006.
[16] N.J. Higham, Accuracy and Stability of Numerical Algorithms. SIAM, 1996.
[17] J.W. Demmel and Y. Hida, “Fast and Accurate Floating Point Summation with Applications to Computational Geometry,” Proc. 10th GAMMIMACS Int'l Symp. Scientific Computing, Computer Arithmetic, and Validated Numerics, 2002.
[18] T. Ogita, S.M. Rump, and S. Oishi, “Accurate Sum and Dot Product,” SIAM J. Scientific Computing, vol. 26, no. 6, pp. 19551988, 2005.
[19] D.M. Priest, “Algorithms for Arbitrary Precision FloatingPoint Arithmetic,” Proc. 10th IEEE Symp. Computer Arithmetic, pp. 132144, 1991.
[20] M. Daumas, “Multiplications of Floating Point Expansions,” Proc. 14th IEEE Symp. Computer Arithmetic, pp. 250257, 1999.
[21] F. de Dinechin, C.Q. Lauter, and J.M. Muller, “Fast and Correctly Rounded Logarithms in Double Precision,” Theoretical Informatics and Applications, vol. 41, no. 1, pp. 85102, 2007.
[22] C.Q. Lauter, “Basic Building Blocks for a TripleDouble Intermediate Format,” Technical Report RR200538, LIP, Sept. 2005.
[23] V. Lefèvre and J.M. Muller, “Worst Cases for Correct Rounding of the Elementary Functions in Double Precision,” Proc. 15th IEEE Symp. Computer Arithmetic, pp. 111118, 2001.