{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,17]],"date-time":"2022-05-17T20:51:40Z","timestamp":1652820700545},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540001164","type":"print"},{"value":"9783540361268","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_17","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"274-291","source":"Crossref","is-referenced-by-count":12,"title":["Mechanical Verification of a Square Root Algorithm Using Taylor\u2019s Theorem"],"prefix":"10.1007","author":[{"given":"Jun","family":"Sawada","sequence":"first","affiliation":[]},{"given":"Ruben","family":"Gamboa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, R. Kaivola, K. R. Kohatsu, and C.-J. H. Seger. Formal verification of iterative algorithms in microprocessors. Proceedings Design Automation Conference (DAC 2000), pages 201\u2013206, 2000.","DOI":"10.1145\/337292.337388"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"R. C. Agarwal, F. G. Gustavson, and M. S. Schmookler. Series approximation methods for divide and square root in the Power3 processor. In Proceedings of the 14th IEEE Symposium on Computer Arithmetic, pages 116\u2013123, 1999.","DOI":"10.1109\/ARITH.1999.762836"},{"key":"17_CR3","unstructured":"W. Fulks. Advanced Calculus: an introduction to analysis. John Wiley & Sons, third edition, 1978."},{"key":"17_CR4","unstructured":"R. Gamboa. Mechanically Verifying Real-Valued Algorithms in ACL2. PhD thesis, University of Texas at Austin, 1999."},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/A:1012912614285","volume":"20","author":"R. Gamboa","year":"2002","unstructured":"R. Gamboa. The correctness of the Fast Fourier Trasnform: A structured proof in ACL2. Formal Methods in System Design, 20:91\u2013106, January 2002.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"17_CR6","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R. Gamboa","year":"2001","unstructured":"R. Gamboa and M. Kaufmann. Nonstandard analysis in ACL2. Journal of Automated Reasoning, 27(4):323\u2013351, November 2001.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR7","unstructured":"R. Gamboa and B. Middleton. Taylor\u2019s formula with remainder. In Proceedings of the Third International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2002), 2002."},{"key":"17_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u201997","author":"J. Harrison","year":"1997","unstructured":"J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u201997, volume 1275 of LNCS, pages 137\u2013152. Springer-Verlag, 1997."},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","first-page":"217","volume-title":"Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000","author":"J. Harrison","year":"2000","unstructured":"J. Harrison. Formal verification of floating point trigonometric functions. In W. A. Hunt and S. D. Johnson, editors, Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, volume 1954 of LNCS, pages 217\u2013233. Springer-Verlag, 2000."},{"key":"17_CR10","unstructured":"Institute of Electrical and Electronic Engineers. IEEE Standard for Binary Floating-Point Arithmetic. ANSI\/IEEE Std 754-1985."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"M. Kaufmann. Modular proof: The fundamental theorem of calculus. In M. Kaufmann, P. Manolios, and J. S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, chapter 6. Kluwer Academic Press, 2000.","DOI":"10.1007\/978-1-4757-3188-0_6"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"M. Kaufmann and J. S. Moore. ACL2: An industrial strength version of nqthm. In Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23\u201334. IEEE Computer Society Press, June 1996.","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"17_CR13","unstructured":"E. Nelson. On-line books: Internal set theory. Available on the world-wide web at http:\/\/www.math.princeton.edu\/~nelson\/books.html ."},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1090\/S0002-9904-1977-14398-X","volume":"83","author":"E. Nelson","year":"1977","unstructured":"E. Nelson. Internal set theory. Bulletin of the American Mathematical Society, 83:1165\u20131198, 1977.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"17_CR15","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, Q1, Feb. 1999."},{"key":"17_CR16","unstructured":"A. Robert. Non-Standard Analysis. John Wiley, 1988."},{"key":"17_CR17","unstructured":"A. Robinson. Model theory and non-standard arithmetic, infinitistic methods. In Symposium on Foundations of Mathematics, 1959."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"D. Russinoff. A Mechanically Checked Proof of Correctness of the AMDK5 Floating-Point Square Root Microcode. Formal Methods in System Design, 14(1), 1999.","DOI":"10.1023\/A:1008669628911"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"D. M. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithm of the AMDK7 Processor. J. Comput. Math. (UK), 1, 1998.","DOI":"10.1112\/S1461157000000176"},{"key":"17_CR20","unstructured":"J. Sawada. ACL2 computed hints: Extension and practice. In ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences, Technical Report TR-00-29, Nov. 2000."},{"key":"17_CR21","unstructured":"J. Sawada. Formal verification of divide and square algorithms using series calculation. Technical Report RC22444, IBM, May 2002."}],"container-title":["Formal Methods in Computer-Aided Design","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:27:00Z","timestamp":1558985220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":21,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-36126-x_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2002]]}}}