{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:30Z","timestamp":1740107970700,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10009-003-0120-y","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T13:53:20Z","timestamp":1079704400000},"page":"237-246","source":"Crossref","is-referenced-by-count":4,"title":["Properties of two\u2019s complement floating point notations"],"prefix":"10.1007","volume":"5","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[]},{"given":"Marc","family":"Daumas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"120_CR1","unstructured":"Amerkad A, Bertot Y, Rideau L, Pottier L (2001) Mathematics and proof presentation in Pcoq. In: Proceedings of the conference on proof transformation and presentation and proof complexities, Siena, Italy. Available at: http:\/\/www-sop.inria.fr\/lemme\/Laurence.Rideau\/proof-pcoq.ps.gz"},{"key":"120_CR2","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/32.24710","volume":"15","author":"G Barrett","year":"1989","unstructured":"Barrett G (1989) Practical algorithm for selection on coarse grained parallel computers. IEEE Trans Softw Eng 15:611\u2013621. http:\/\/dlib.computer.org\/ts\/books\/ts1989\/pdf\/e0611.pdf","journal-title":"IEEE Trans Softw Eng"},{"key":"120_CR3","doi-asserted-by":"crossref","unstructured":"Boldo S, Daumas M (2002) Properties of the subtraction valid for any floating point system. In: Proceedings of the 7th international workshop on formal methods for industrial critical systems, M\u00e1laga, Spain, pp 137\u2013149","DOI":"10.1016\/S1571-0661(04)80408-0"},{"key":"120_CR4","doi-asserted-by":"crossref","unstructured":"Carre\u00f1o VA, Miner PS (1995) Specification of the IEEE-854 floating-point standard in HOL and PVS. In: Proceedings of the 1995 international workshop on higher order logic theorem proving and its applications, Aspen Grove, UT, supplemental proceedings. Available at: http:\/\/shemesh.larc.nasa.gov\/fm\/ftp\/larc\/vac\/hug95.ps","DOI":"10.1016\/S1474-6670(17)44820-8"},{"key":"120_CR5","doi-asserted-by":"crossref","unstructured":"Chen YA, Clarke E, Ho PH, Hoskote Y, Kam T, Khaira M, O\u2019Leary J, Zhao X (1996) Verification of all circuits in a floating point unit using word level model checking. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design, Palo Alto, CA, pp 19\u201333","DOI":"10.1007\/BFb0031797"},{"key":"120_CR6","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/MM.1984.291224","volume":"4","author":"Cody","year":"1984","unstructured":"Cody WJ, Karpinski R et al (1984) A proposed radix and word-length independent standard for floating point arithmetic. IEEE Micro 4:86\u2013100","journal-title":"IEEE Micro"},{"key":"120_CR7","unstructured":"Collins RR (1997) Inside the Pentium II math bug. Dr. Dobb\u2019s Journal 22(8):52, 55\u201357. Available at: http:\/\/www.ddj.com\/articles\/1997\/9708\/9708f\/9708f.htm"},{"key":"120_CR8","unstructured":"Coonen JT (1978) Specification for a proposed standard for floating point arithmetic. Memorandum ERL M78\/72, University of California, Berkeley"},{"key":"120_CR9","doi-asserted-by":"crossref","unstructured":"Cowlishaw MF (2003) Decimal floating point: algorithm for computers. In: Bajard JC, Schulte M (eds) Proceedings of the 16th symposium on computer arithmetic, Santiago de Compostela, Spain, 2003, pp 104\u2013111. Available at: http:\/\/csdl.computer.org\/comp\/proceedings\/arith\/2003\/1894\/00\/1894toc.htm","DOI":"10.1109\/ARITH.2003.1207666"},{"key":"120_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/S0304-3975(02)00223-2","volume":"291","author":"M Daumas","year":"2003","unstructured":"Daumas M, Langlois P (2003) Additive symmetries: the non-negative case. Theor Comput Sci 291:143\u2013157. Available at: http:\/\/dx.doi.org\/10.1016\/S0304-3975(02)00223-2","journal-title":"Theor Comput Sci"},{"key":"120_CR11","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1109\/12.589241","volume":"46","author":"Daumas","year":"1997","unstructured":"Daumas M, Matula DW (1997) Validated roundings of dot products by sticky accumulation. IEEE Trans Comput 46:623\u2013629.","journal-title":"IEEE Trans Comput"},{"key":"120_CR12","doi-asserted-by":"crossref","unstructured":"Daumas M, Rideau L, Th\u00e9ry L (2001) A generic library of floating-point numbers and its application to exact computing. In: Proceedings of the 14th international conference on theorem proving in higher order logics. Edinburgh, UK, pp 169\u2013184.","DOI":"10.1007\/3-540-44755-5_13"},{"key":"120_CR13","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1137\/0905062","volume":"5","author":"Demmel","year":"1984","unstructured":"Demmel J (1984) Underflow and the reliability of numerical software. SIAM J Sci Stat Comput 5:887\u2013919","journal-title":"SIAM J Sci Stat Comput"},{"key":"120_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D Goldberg","year":"1991","unstructured":"Goldberg D (1991) What every computer scientist should know about floating point arithmetic. ACM Comput Surv 23:5\u201347. Available at: http:\/\/www.acm.org\/pubs\/articles\/journals\/surveys\/1991-23-1\/p5-goldberg\/p5-goldberg.pdf","journal-title":"ACM Comput Surv"},{"key":"120_CR15","doi-asserted-by":"crossref","unstructured":"Harrison J (1999) A machine-checked theory of floating point arithmetic. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Th\u00e9ry L (eds) Proceedings of the 12th international conference on theorem proving in higher order logics, Nice, France, pp 113\u2013130. Available at: http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/fparith.ps.gz","DOI":"10.1007\/3-540-48256-3_9"},{"key":"120_CR16","doi-asserted-by":"crossref","unstructured":"Harrison J (2000) Formal verification of floating point trigonometric functions. In: Hunt WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design, Austin, TX, pp 217\u2013233. Available at: http:\/\/www.link.springer.de\/link\/service\/series\/0558\/papers\/1954\/19540217.pdf","DOI":"10.1007\/3-540-40922-X_14"},{"key":"120_CR17","unstructured":"Higham NJ (1996) Accuracy and stability of numerical algorithms. SIAM, Philadelphia. Available at: http:\/\/www.ma.man.ac.uk\/\u223chigham\/asna.html. Also at: http:\/\/www.maths.man.ac.uk\/\u223chigham\/asna\/"},{"key":"120_CR18","unstructured":"Huet G, Kahn G, Paulin-Mohring C (1997) The Coq proof assistant: a tutorial: version 6.1. Technical Report 204, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France. Available at: ftp:\/\/ftp.inria.fr\/INRIA\/publication\/publi-pdf\/RT\/RT-0204.pdf"},{"key":"120_CR19","unstructured":"Jacobi C (2001) Formal verification of a theory of IEEE rounding. In: Proceedings of the 14th international conference on theorem proving in higher order logics, Edinburgh, UK, pp 239\u2013254, supplemental proceedings. Available at: http:\/\/www.informatics.ed.ac.uk\/publications\/online\/0046\/b239.pdf"},{"key":"120_CR20","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern C, Greenstreet MR (1999) Formal verification in hardware design: a survey. ACM Trans Des Automat Electron Sys 4:123\u2013193. Available at: http:\/\/delivery.acm.org\/10.1145\/310000\/307989\/p123-kern.pdf","journal-title":"ACM Trans Des Automat Electron Sys"},{"key":"120_CR21","first-page":"seminumerical","volume":"programming","author":"Knuth","year":"1997","unstructured":"Knuth DE (1997) The art of computer programming: seminumerical algorithms, 3rd edn. Addison-Wesley, Reading, MA","journal-title":"The art of computer"},{"key":"120_CR22","unstructured":"Kulisch U (2000) Rounding near zero. In: Proceedings of the 4th real numbers and computers conference, Dagstuhl, Germany, pp 23\u201329"},{"key":"120_CR23","doi-asserted-by":"crossref","unstructured":"Laurent O, Michel P, Wiels V (2001) Using formal verification techniques to reduce simulation and test effort. In: Proceedings of the international symposium of formal methods Europe, Berlin, Germany, pp 465\u2013477. Available at: http:\/\/link.springer.de\/link\/service\/series\/0558\/papers\/2021\/20210465.pdf","DOI":"10.1007\/3-540-45251-6_27"},{"key":"120_CR24","doi-asserted-by":"crossref","unstructured":"Li RC, Boldo S, Daumas M (2003) Theorems on efficient argument reductions. In: Bajard JC, Schulte M (eds) Proceedings of the 16th symposium on computer arithmetic, Santiago de Compostela, Spain, pp 129\u2013136.","DOI":"10.1109\/ARITH.2003.1207670"},{"key":"120_CR25","unstructured":"Markstein P (2000) IA-64 and elementary functions: speed and precision. Prentice Hall, Upper Saddle River, NJ. Available at: http:\/\/www.markstein.org\/"},{"key":"120_CR26","doi-asserted-by":"crossref","unstructured":"Miner PS, Leathrum JF (1996) Verification of IEEE compliant subtractive division algorithms. In: Proceedings of the 1st international conference on formal methods in computer-aided design, pp 64\u201378. Available at: http:\/\/www.ece.odu.edu\/\u223cleathrum\/Formal_Methods\/computer_arithmetic\/fmcad.ps","DOI":"10.1007\/BFb0031800"},{"key":"120_CR27","unstructured":"O\u2019Leary J, Zhao X, Gerth R, Seger CJH (1999) Formally verifying IEEE compliance of floating point hardware. Intel Technol J, vol 3. Available at: http:\/\/developer.intel.com\/technology\/itj\/q11999\/pdf\/floating_point.pdf"},{"key":"120_CR28","doi-asserted-by":"crossref","unstructured":"Overton MJ (2001) Numerical computing with IEEE floating point arithmetic. SIAM, Philadelphia. Available at: http:\/\/www.siam.org\/catalog\/mcc07\/ot76.htm","DOI":"10.1137\/1.9780898718072"},{"key":"120_CR29","unstructured":"Priest DM (1992) On properties of floating point arithmetics: numerical stability and the cost of accurate computations. PhD thesis, University of California at Berkeley, Berkeley, CA. Available at: ftp:\/\/ftp.icsi.berkeley.edu\/pub\/theory\/priest-thesis.ps.Z"},{"key":"120_CR30","doi-asserted-by":"crossref","unstructured":"Rushby J, von Henke F (1991) Formal verification of algorithms for critical systems. In: Proceedings of the conference on software for critical systems, New Orleans, pp 1\u201315. Available at: http:\/\/www.acm.org\/pubs\/articles\/proceedings\/soft\/125083\/p1-rushby\/p1-rushby.pdf","DOI":"10.1145\/125083.123044"},{"key":"120_CR31","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"DM Russinoff","year":"1998","unstructured":"Russinoff DM (1998) A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J Comput Math 1:148\u2013200. http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.ps","journal-title":"LMS J Comput Math"},{"key":"120_CR32","unstructured":"Schryer NL (1981) A test of computer\u2019s floating-point arithmetic unit. Technical report 89, AT&T Bell Laboratories. Available at: http:\/\/cm.bell-labs.com\/cm\/cs\/cstr\/89.ps.gz"},{"key":"120_CR33","doi-asserted-by":"crossref","unstructured":"Schwarz EM, Smith RM, Krygowski CA (1999) The S\/390 G5 floating point unit supporting hex and binary architectures. In: Koren I, Kornerup P (eds) Proceedings of the 14th symposium on computer arithmetic, Adelaide, Australia, pp 258\u2013265 . Available at: http:\/\/computer.org\/proceedings\/arith\/0116\/0116toc.htm","DOI":"10.1109\/ARITH.1999.762852"},{"key":"120_CR34","unstructured":"Sterbenz PH (1974) Floating point computation. Prentice-Hall, Upper Saddle River, NJ"},{"key":"120_CR35","first-page":"9","volume":"22","author":"Stevenson","year":"1987","unstructured":"Stevenson D et al (1987) An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices 22:9\u201325","journal-title":"ACM SIGPLAN Notices"},{"key":"120_CR36","unstructured":"Texas Instruments (1997) TMS320C3x User\u2019s guide. Available at: http:\/\/www-s.ti.com\/sc\/psheets\/spru031e\/spru031e.pdf"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0120-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0120-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0120-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0120-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:18Z","timestamp":1559100318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0120-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":36,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["120"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0120-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}