{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T18:03:56Z","timestamp":1717697036219},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,4,13]],"date-time":"2010-04-13T00:00:00Z","timestamp":1271116800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s11334-010-0128-x","type":"journal-article","created":{"date-parts":[[2010,4,12]],"date-time":"2010-04-12T10:36:43Z","timestamp":1271068603000},"page":"173-179","source":"Crossref","is-referenced-by-count":4,"title":["Improved bound for stochastic formal correctness of numerical algorithms"],"prefix":"10.1007","volume":"6","author":[{"given":"Marc","family":"Daumas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Lester","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annick","family":"Truffert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,4,13]]},"reference":[{"key":"128_CR1","doi-asserted-by":"crossref","unstructured":"Audebaud P, Paulin-Mohring C (2006) Proofs of randomized algorithms in Coq. In: Uustalu T (ed) Proceedings of the 8th international conference on mathematics of program construction. Kuressaare, Estonia, pp 49\u201368. doi: 10.1007\/11783596_6","DOI":"10.1007\/11783596_6"},{"key":"128_CR2","unstructured":"Bertoin J (2001) Probabilit\u00e9s. http:\/\/www.proba.jussieu.fr\/cours\/bertoin.pdf . Cours de licence de math\u00e9matiques appliqu\u00e9es"},{"key":"128_CR3","doi-asserted-by":"crossref","unstructured":"Boldo S, Daumas M (2003) Representable correcting terms for possibly underflowing floating point operations. In: Bajard JC, Schulte M (eds) Proceedings of the 16th symposium on computer arithmetic. Santiago de Compostela, Spain, pp 79\u201386. http:\/\/perso.ens-lyon.fr\/marc.daumas\/SoftArith\/BolDau03.pdf","DOI":"10.1109\/ARITH.2003.1207663"},{"key":"128_CR4","doi-asserted-by":"crossref","unstructured":"Boldo S, Mu\u00f1oz C (2006) Provably faithful evaluation of polynomials. In: Proceedings of the 2006 ACM symposium on applied computing. Dijon, France, pp 1328\u20131332. doi: 10.1145\/1141277.1141586","DOI":"10.1145\/1141277.1141586"},{"issue":"4","key":"128_CR5","doi-asserted-by":"crossref","first-page":"716","DOI":"10.1145\/322154.322162","volume":"26","author":"J Bustoz","year":"1979","unstructured":"Bustoz J, Feldstein A, Goodman R, Linnainmaa S (1979) Improved trailing digits estimates applied to optimal computer arithmetic. J ACM 26(4):716\u2013730. doi: 10.1145\/322154.322162","journal-title":"J ACM"},{"key":"128_CR6","first-page":"19","volume-title":"Study of the computing accuracy by using probabilistic approach","author":"JM Chesneaux","year":"1990","unstructured":"Chesneaux JM (1990) Contribution to computer arithmetic and self-validating numerical methods. In: Ullrich C (eds) Study of the computing accuracy by using probabilistic approach. Baltzer, Basel, pp 19\u201330"},{"key":"128_CR7","doi-asserted-by":"crossref","unstructured":"Daumas M, Lester D (2007) Stochastic formal methods: an application to accuracy of numeric software. In: Proceedings of the 40th IEEE annual Hawaii international conference on system sciences, p 7. Waikoloa, Hawaii. http:\/\/hal.ccsd.cnrs.fr\/ccsd-00081413","DOI":"10.1109\/HICSS.2007.499"},{"key":"128_CR8","unstructured":"Daumas M, Lester D, Martin-Dorel \u00c9, Truffert A (2009) Stochastic formal correctness of numerical algorithms. In: NASA formal methods symposium, pp 136\u2013145. http:\/\/ti.arc.nasa.gov\/m\/event\/nfm09\/NFM09Proceedings.pdf"},{"issue":"2","key":"128_CR9","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas M, Lester D, Mu\u00f1oz C (2009) Verified real number calculations: a library for interval arithmetic. IEEE Trans Comput 58(2): 226\u2013237. doi: 10.1109\/TC.2008.213","journal-title":"IEEE Trans Comput"},{"key":"128_CR10","doi-asserted-by":"crossref","unstructured":"Daumas M, Melquiond G (2010) Certification of bounds on expressions involving rounded operators. ACM Trans Math Softw 37(1). http:\/\/hal.archives-ouvertes.fr\/hal-00127769 (to appear)","DOI":"10.1145\/1644001.1644003"},{"issue":"2","key":"128_CR11","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1145\/321941.321948","volume":"23","author":"A Feldstein","year":"1976","unstructured":"Feldstein A, Goodman R (1976) Convergence estimates for the distribution of trailing digits. J ACM 23(2): 287\u2013297. doi: 10.1145\/321941.321948","journal-title":"J ACM"},{"issue":"1","key":"128_CR12","doi-asserted-by":"crossref","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(1): 5\u201347. doi: 10.1145\/103162.103163","journal-title":"ACM Comput Surv"},{"key":"128_CR13","volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","unstructured":"Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge"},{"key":"128_CR14","doi-asserted-by":"crossref","unstructured":"Harrison J (2000) Formal verification of floating point trigonometric functions. In: Hunt WA, Johnson SD (eds) Proceedings of the third international conference on formal methods in computer-aided design, pp 217\u2013233. Austin, Texas. http:\/\/www.springerlink.com\/link.asp?id=wxvaqu9wjrgc8l99","DOI":"10.1007\/3-540-40922-X_14"},{"key":"128_CR15","unstructured":"Huet G, Kahn G, Paulin-Mohring C (2009) The Coq proof assistant: a tutorial: version 8.2. http:\/\/coq.inria.fr\/distrib\/current\/files\/Tutorial.pdf"},{"key":"128_CR16","unstructured":"Hurd J (2002) Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge. http:\/\/www.cl.cam.ac.uk\/~jeh1004\/research\/papers\/thesis.pdf"},{"key":"128_CR17","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht"},{"key":"128_CR18","volume-title":"The art of computer programming: seminumerical algorithms","author":"DE Knuth","year":"1997","unstructured":"Knuth DE (1997) The art of computer programming: seminumerical algorithms, 3rd edn. Addison-Wesley, Reading","edition":"3"},{"key":"128_CR19","volume-title":"Martingales \u00e0 temps discret","year":"1972","unstructured":"Neveu J (ed) (1972) Martingales \u00e0 temps discret. Masson, Paris"},{"key":"128_CR20","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th international conference on automated deduction. Springer, Saratoga, New York, pp 748\u2013752. http:\/\/pvs.csl.sri.com\/papers\/cade92-pvs\/cade92-pvs.ps","DOI":"10.1007\/3-540-55602-8_217"},{"key":"128_CR21","doi-asserted-by":"crossref","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","DOI":"10.1112\/S1461157000000176"},{"issue":"2","key":"128_CR22","first-page":"9","volume":"22","author":"D Stevenson","year":"1987","unstructured":"Stevenson D et\u00a0al (1987) An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices 22(2): 9\u201325","journal-title":"ACM SIGPLAN Notices"},{"key":"128_CR23","unstructured":"Texas Instruments (1997) TMS320C3x\u2014user\u2019s guide. http:\/\/www.s.ti.com\/sc\/psheets\/spru031e\/spru031e.pdf"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-010-0128-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-010-0128-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-010-0128-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T09:47:45Z","timestamp":1559382465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-010-0128-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,13]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["128"],"URL":"https:\/\/doi.org\/10.1007\/s11334-010-0128-x","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,13]]}}}