{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:05:59Z","timestamp":1773655559308,"version":"3.50.1"},"reference-count":32,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.3103\/s0146411619070186","type":"journal-article","created":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T10:02:40Z","timestamp":1583316160000},"page":"595-616","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Platform-Independent Specification and Verification of the Standard Mathematical Square Root Function"],"prefix":"10.3103","volume":"53","author":[{"given":"N. V.","family":"Shilov","sequence":"first","affiliation":[]},{"given":"D. A.","family":"Kondratyev","sequence":"additional","affiliation":[]},{"given":"I. S.","family":"Anureev","sequence":"additional","affiliation":[]},{"given":"E. V.","family":"Bodin","sequence":"additional","affiliation":[]},{"given":"A. V.","family":"Promsky","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2020,3,4]]},"reference":[{"key":"7161_CR1","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1134\/S036176880703005X","volume":"33","author":"V.V. Kuliamin","year":"2007","unstructured":"Kuliamin, V.V., Standardization and testing of implementations of mathematical functions in floating point numbers, Program. Comput. Software, 2007, vol. 33, no. 3, pp. 154\u2013173.","journal-title":"Program. Comput. Software"},{"key":"7161_CR2","unstructured":"Nikitin, V.F., A variant for calculating the square root (Newton\u2019s algorithm). http:\/\/algolist.manual.ru\/ maths\/count_fast\/sqrt.php."},{"key":"7161_CR3","unstructured":"Shelekhov, V.I., Verification and synthesis of effective programs of standard functions floor, isqrt, and ilog2 in predicate programming technology, Problemy upravleniya i modelirovaniya v slozhnykh sistemakh, Trudy 12-i mezhd. konf. (Problems of Control and Modeling in Complex Systems, Proc. 12th Int. Conf.), Samara, 2010, pp. 622\u2013630."},{"key":"7161_CR4","first-page":"127","volume":"6173","author":"A. Ayad","year":"2010","unstructured":"Ayad, A. and March\u00e9, C., Multi-prover verification of floating-point programs, Perspectives of System Informatics. PSI 2014; Lect. Notes Artif. Intell., 2010, vol. 6173, pp. 127\u2013141.","journal-title":"Lect. Notes Artif. Intell."},{"key":"7161_CR5","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"G. Barret","year":"1989","unstructured":"Barret, G., Formal methods applied to a floating-point number system, IEEE Trans. Software Eng., 1989, vol.\u00a015, no. 5, pp. 611\u2013621.","journal-title":"IEEE Trans. Software Eng."},{"key":"7161_CR6","doi-asserted-by":"crossref","unstructured":"Brain, M., et al., An automatable formal semantics for IEEE-754 floating-point arithmetic, Computer Arithmetic (ARITH \u201815), Proc. of the 2015 IEEE 22nd Symposium (IEEE Computer Society), 2015, pp. 160\u2013167.","DOI":"10.1109\/ARITH.2015.26"},{"key":"7161_CR7","unstructured":"El-Magdoub, M.H., Best Square Root Method\u2013Algorithm\u2013Function (Precision VS Speed). https:\/\/www. codeproject.com\/Articles\/69941\/Best-Square-Root-Method-Algorithm-Function-Precisi."},{"key":"7161_CR8","unstructured":"Ferguson, W.E., et al., Digit serial methods with applications to division and square root (with mechanically checked correctness proofs), arXiv: arXiv:1708.00140, 2017, pp. 102\u2013114."},{"key":"7161_CR9","volume-title":"Square Roots in Acl2: A Study in Sonata Form, Technical Report","author":"R.A. Gamboa","year":"1997","unstructured":"Gamboa, R.A., Square Roots in Acl2: A Study in Sonata Form, Technical Report, University of Texas at Austin, 1997."},{"key":"7161_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D., The Science of Programming, New York: Springer-Verlag, 1981."},{"key":"7161_CR11","unstructured":"Grohoski, G., Verifying Oracle\u2019s SPARC processors with ACL2 (slides of the invited talk), The ACL2 Theorem Prover and Its Applications, Proc. Int. Workshop, 2017. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2017\/slides-accepted\/grohoski-ACL2_talk.pdf."},{"key":"7161_CR12","unstructured":"Gutowski, M.W., Power and beauty of interval methods, arXiv: arXiv:physics\/0302034."},{"key":"7161_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume":"1690","author":"J. Harrison","year":"1999","unstructured":"Harrison, J., A machine-checked theory of floating point arithmetic, Lect. Notes Comput. Sci., 1999, vol. 1690, pp. 113\u2013130.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-40922-X_13","volume":"1954","author":"J. Harrison","year":"2000","unstructured":"Harrison, J., Formal verification of floating point trigonometric functions, Lect. Notes Comput. Sci., 2000, vol.\u00a01954, pp. 217\u2013251.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR15","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-44659-1_15","volume":"1869","author":"J. Harrison","year":"2000","unstructured":"Harrison, J., Formal verification of IA-64 division algorithms, Lect. Notes Comput. Sci., 2000, vol. 1869, pp.\u00a0233\u2013251.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR16","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1008712907154","volume":"16","author":"J. Harrison","year":"2000","unstructured":"Harrison, J., Floating point verification in HOL light: The exponential function, Formal Methods Syst. Des., 2000, vol. 16, no. 3, pp. 271\u2013305.","journal-title":"Formal Methods Syst. Des."},{"key":"7161_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J. Harrison","year":"2003","unstructured":"Harrison, J., Formal verification of square root algorithms, Formal Methods Syst. Des., 2003, vol. 22, no. 2, pp.\u00a0143\u2013153.","journal-title":"Formal Methods Syst. Des."},{"key":"7161_CR18","first-page":"1","volume":"2890","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R., The verifying compiler: A grand challenge for computing research, Lect. Notes Comput. Sci., 2003, vol. 2890, pp. 1\u201312.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR19","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-11486-1_22","volume":"5947","author":"V.V. Kuliamin","year":"2010","unstructured":"Kuliamin, V.V., Standardization and testing of mathematical functions in floating point numbers, Lect. Notes Comput. Sci., 2010, vol. 5947, pp. 257\u2013268.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D. Monniaux","year":"2008","unstructured":"Monniaux, D., The pitfalls of verifying floating-point computations, ACM Trans. Program. Languages Syst., 2008, vol. 30, no. 3, pp. 1\u201341.","journal-title":"ACM Trans. Program. Languages Syst."},{"key":"7161_CR21","volume-title":"Elementary Functions: Algorithms and Implementation","author":"J.-M. Muller","year":"2005","unstructured":"Muller, J.-M., Elementary Functions: Algorithms and Implementation, Birkh\u00e4user, 2005."},{"key":"7161_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-76526-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"J.-M. Muller","year":"2018","unstructured":"Muller, J.-M., et al., Handbook of Floating-Point Arithmetic, Birkh\u00e4user, 2018, 2nd ed."},{"key":"7161_CR23","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-36126-X_17","volume":"2517","author":"J. Sawada","year":"2002","unstructured":"Sawada, J. and Gamboa, R., Mechanical verification of a square root algorithm using Taylor\u2019s theorem, Lect. Notes Comput. Sci., 2002, vol. 2517, pp. 274\u2013291.","journal-title":"Lect. Notes Comput. Sci."},{"key":"7161_CR24","unstructured":"Shilov, N.V., On the need to specify and verify standard functions, Bull. Novosib. Comput. Center (Ser.: Comput. Sci.), 2015, vol. 38, pp. 105\u2013119."},{"key":"7161_CR25","first-page":"57","volume":"19","author":"N.V. Shilov","year":"2016","unstructured":"Shilov, N.V. and Promsky, A.V., On specification and verification of standard mathematical functions, Humanit. Sci. Univ. J., 2016, vol. 19, pp. 57\u201368.","journal-title":"Humanit. Sci. Univ. J."},{"key":"7161_CR26","unstructured":"Shilov, N.V., et al., Towards platform-independent verification of the standard mathematical functions: The square root function, arXiv: arXiv:abs\/1801.00969."},{"key":"7161_CR27","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/s10817-014-9311-3","volume":"53","author":"U. Siddique","year":"2014","unstructured":"Siddique, U. and Hasan, O., On the formalization of gamma function in HOL, J. Autom. Reason., 2014, vol. 53, no. 4, pp. 407\u2013429.","journal-title":"J. Autom. Reason."},{"key":"7161_CR28","unstructured":"C reference. Sqrt, sqrtf, sqrtl. http:\/\/en.cppreference.com\/w\/c\/numeric\/math\/sqrt."},{"key":"7161_CR29","unstructured":"IEEE 754-2008. http:\/\/ieeexplore.ieee.org\/document\/4610935."},{"key":"7161_CR30","unstructured":"ISO\/IEC\/IEEE 60559:2011. Information Technology \u2013 Microprocessor Systems \u2013 Floating-Point arithmetic. http:\/\/www.iso.org\/iso\/iso_catalogue\/catalogue_tc\/catalogue_detail.htm?csnumber=57469."},{"key":"7161_CR31","unstructured":"nth root algorithm. https:\/\/en.wikipedia.org\/wiki\/Nth_root_algorithm."},{"key":"7161_CR32","unstructured":"Roskosmos named reason for failured launch from space center Vostochny. https:\/\/www.rbc.ru\/politics\/ 12\/12\/2017\/5a2ebcd59a79479d29667115."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070186.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411619070186","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070186.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:52Z","timestamp":1773611872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411619070186"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":32,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["7161"],"URL":"https:\/\/doi.org\/10.3103\/s0146411619070186","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12]]},"assertion":[{"value":"10 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2018","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 November 2018","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}