{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T09:17:31Z","timestamp":1780996651609,"version":"3.54.1"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1023\/a:1022973506233","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"143-153","source":"Crossref","is-referenced-by-count":21,"title":["Formal Verification of Square Root Algorithms"],"prefix":"10.1007","volume":"22","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5117030_CR1","doi-asserted-by":"crossref","unstructured":"M. Aigner and G.M. Ziegler, Proofs from The Book, Springer-Verlag, 2nd edition. 2001.","DOI":"10.1007\/978-3-662-04315-8"},{"key":"5117030_CR2","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K. Appel","year":"1976","unstructured":"K. Appel and W. Haken, \u201cEvery planar map is four colorable,\u201d Bulletin of the American Mathematical Society Vol. 82, pp. 711\u2013712, 1976.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"5117030_CR3","unstructured":"M. Cornea-Hasegan, \u201cProving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms,\u201d Intel Technology Journal 1998-Q2, 1\u201311. Available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q21998\/articles\/art_3.htm."},{"key":"5117030_CR4","doi-asserted-by":"crossref","unstructured":"G. Cousineau and M. Mauny, The Functional Approach to Programming, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"key":"5117030_CR5","first-page":"194","volume":"5","author":"P. Erd\u00f6s","year":"1930","unstructured":"P. Erd\u00f6s, \u201cBeweis eines Satzes von Tschebyshev,\u201d Acta Scientiarum Mathematicarum (Szeged),Vol. 5, pp. 194\u2013198, 1930.","journal-title":"Acta Scientiarum Mathematicarum (Szeged)"},{"key":"5117030_CR6","volume-title":"Applications of division by convergence","author":"R.E. Goldschmidt","year":"1964","unstructured":"R.E. Goldschmidt, \u201cApplications of division by convergence,\u201d Master's thesis, Dept. of Electrical Engineering, MIT, Cambridge, Mass, 1964."},{"key":"5117030_CR7","unstructured":"M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"5117030_CR8","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon, R. Milner, and C.P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Vol. 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"5117030_CR9","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cHOL Light: A Tutorial Introduction,\u201d in M. Srivas and A. Camilleri (eds.), in Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Vol. 1166 of Lecture Notes in Computer Science. 1996, pp. 265\u2013269.","DOI":"10.1007\/BFb0031814"},{"key":"5117030_CR10","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cVerifying the accuracy of polynomial approximations in HOL,\u201d in E.L. Gunter and A. Felty (eds.), Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Vol. 1275 of Lecture Notes in Computer Science. Murray Hill, NJ, 1997, pp. 137\u2013152.","DOI":"10.1007\/BFb0028391"},{"key":"5117030_CR11","doi-asserted-by":"crossref","unstructured":"J. Harrison, Theorem Proving with the Real Numbers, Springer-Verlag, Revised version of author's PhD thesis, 1998.","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"5117030_CR12","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cA machine-checked theory of floating point arithmetic,\u201d in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry (eds.), Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99, Vol. 1690 of Lecture Notes in Computer Science. Nice, France, 1999, pp. 113\u2013130.","DOI":"10.1007\/3-540-48256-3_9"},{"key":"5117030_CR13","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cFormal verification of floating point trigonometric functions,\u201d in W.A. Hunt and S.D. Johnson (eds.), Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, Vol. 1954 of Lecture Notes in Computer Science. 2000, pp. 217\u2013233.","DOI":"10.1007\/3-540-40922-X_14"},{"key":"5117030_CR14","doi-asserted-by":"crossref","unstructured":"J. Harrison, \u201cFormal verification of IA-64 division algorithms,\u201d in M. Aagaard and J. Harrison (eds.), Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, Vol. 1869 of Lecture Notes in Computer Science. 2000, pp. 234\u2013251.","DOI":"10.1007\/3-540-44659-1_15"},{"key":"5117030_CR15","unstructured":"IEEE: 1985, \u201cStandard for binary floating point arithmetic,\u201d ANSI\/IEEE Standard 754\u20131985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA."},{"key":"5117030_CR16","unstructured":"P. Markstein, IA-64 and Elementary Functions: Speed and Precision, Prentice-Hall, 2000."},{"key":"5117030_CR17","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P.W. Markstein","year":"1990","unstructured":"P.W. Markstein, \u201cComputation of elementary functions on the IBM RISC System\/6000 processor,\u201d IBM Journal of Research and Development, Vol. 34, pp. 111\u2013119, 1990.","journal-title":"IBM Journal of Research and Development"},{"key":"5117030_CR18","unstructured":"J. O'Leary, X. Zhao, R. Gerth, and C.-J.H. Seger, \u201cFormally Verifying IEEE Compliance of Floating-Point Hardware,\u201d Intel Technology Journal. 1999-Q1, 1\u201314. Available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm."},{"key":"5117030_CR19","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"D. Rusinoff, \u201cA mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions,\u201d LMS Journal of Computation and Mathematics Vol. 1, pp. 148\u2013200, 1998. Available on the Web via http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html.","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"5117030_CR20","doi-asserted-by":"crossref","unstructured":"J. Sawada and R. Gamboa, \u201cMechanical Verification of a Square Root Algorithms using Taylor's Theorem,\u201d in M. Aagaard and J. O'Leary (eds.), Formal Methods in Computer-Aided Design: Fourth International Conference FMCAD 2002, Vol. 2517 of Lecture Notes in Computer Science, 2002.","DOI":"10.1007\/3-540-36126-X_17"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022973506233.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022973506233\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022973506233.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:10:01Z","timestamp":1754421001000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022973506233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["5117030"],"URL":"https:\/\/doi.org\/10.1023\/a:1022973506233","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}