{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:27Z","timestamp":1763468247396},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,12,6]],"date-time":"2014-12-06T00:00:00Z","timestamp":1417824000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10817-014-9317-x","type":"journal-article","created":{"date-parts":[[2014,12,8]],"date-time":"2014-12-08T14:07:47Z","timestamp":1418047667000},"page":"135-163","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Verified Compilation of Floating-Point Computations"],"prefix":"10.1007","volume":"54","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,12,6]]},"reference":[{"key":"9317_CR1","doi-asserted-by":"crossref","unstructured":"Ayad, A., March\u00e9, C.: Multi-prover verification of floating-point programs. In: Giesl, J., H\u00e4hnle, R. (eds.) 5th international joint conference on automated reasoning (IJCAR), Lecture Notes in Computer Science, vol. 6173. Springer, Edinburgh (2010)","DOI":"10.1007\/978-3-642-14203-1_11"},{"key":"9317_CR2","unstructured":"Boldo, S.: Preuves formelles en arithm\u00e9tiques \u00e0 virgule flottante. Ph.D. thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon (2004)"},{"key":"9317_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.C.: Formal verification of floating-point programs. In: Kornerup, P., Muller, J.M. (eds.) 18th IEEE International symposium on computer arithmetic (ARITH). IEEE, pp. 187\u2013194, Montpellier (2007)","DOI":"10.1109\/ARITH.2007.20"},{"issue":"4","key":"9317_CR4","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1109\/TC.2007.70819","volume":"57","author":"S Boldo","year":"2008","unstructured":"Boldo, S., Melquiond, G.: Emulation of FMA and correctly-rounded sums: Proved algorithms using rounding to odd. IEEE Trans. Comput. 57(4), 462\u2013471 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"9317_CR5","first-page":"243","volume-title":"20th IEEE symposium on computer arithmetic","author":"S Boldo","year":"2011","unstructured":"Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) 20th IEEE symposium on computer arithmetic, pp. 243\u2013252. IEEE, T\u00fcbingen (2011)"},{"key":"9317_CR6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s11334-011-0151-6","volume":"7","author":"S Boldo","year":"2011","unstructured":"Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. 7, 151\u2013160 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"issue":"8","key":"9317_CR7","doi-asserted-by":"crossref","first-page":"1069","DOI":"10.1109\/TC.2004.37","volume":"53","author":"N Brisebarre","year":"2004","unstructured":"Brisebarre, N., Muller, J.M., Raina, S.K.: Accelerating correctly rounded floating-point division when the divisor is known in advance. IEEE Trans. Comput. 53(8), 1069\u20131072 (2004)","journal-title":"IEEE Trans. Comput."},{"key":"9317_CR8","unstructured":"Carre\u00f1o, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS In: 8th international workshop on higher-order logic theorem proving and its applications (HOL95), Aspen Grove, UT (1995)"},{"key":"9317_CR9","doi-asserted-by":"crossref","unstructured":"Clinger, W.D.: How to read floating-point numbers accurately In: Programming language design and implementation (PLDI\u201990), pp. 92\u2013101. ACM (1990)","DOI":"10.1145\/93542.93557"},{"key":"9317_CR10","first-page":"21","volume-title":"In: 14th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 3444","author":"P Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyzer In: 14th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 3444, pp. 21\u201330. Springer, Berlin Heidelberg New York (2005)"},{"issue":"3","key":"9317_CR11","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/BF01397083","volume":"18","author":"TJ Dekker","year":"1971","unstructured":"Dekker, T.J.: A floating point technique for extending the available precision. Numerische Mathematik 18(3), 224\u2013242 (1971)","journal-title":"Numerische Mathematik"},{"key":"9317_CR12","first-page":"53","volume-title":"In: Formal methods for industrial critical systems (FMICS), Lecture Notes in Computer Science, vol. 5825","author":"D Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software In: Formal methods for industrial critical systems (FMICS), Lecture Notes in Computer Science, vol. 5825, pp. 53\u201369. Springer, Berlin Heidelberg New York (2009)"},{"issue":"3","key":"9317_CR13","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/221332.221334","volume":"30","author":"SA Figueroa","year":"1995","unstructured":"Figueroa, S.A.: When is double rounding innocuous?. SIGNUM Newsl. 30(3), 21\u201326 (1995)","journal-title":"SIGNUM Newsl."},{"issue":"1","key":"9317_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D Goldberg","year":"1991","unstructured":"Goldberg, D.: What every computer scientist should know about floating point arithmetic. ACM Comput. Surv. 23(1), 5\u201347 (1991)","journal-title":"ACM Comput. Surv."},{"key":"9317_CR15","doi-asserted-by":"crossref","unstructured":"Granlund, T., Montgomery, P.L.: Division by invariant integers using multiplication In: Programming language design and implementation (PLDI\u201994), pp. 61\u201372. ACM (1994)","DOI":"10.1145\/773473.178249"},{"key":"9317_CR16","first-page":"113","volume-title":"In: 12th International conference on theorem proving in higher order logics (TPHOLs\u201999), Lecture Notes in Computer Science, vol. 1690","author":"J Harrison","year":"1999","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) In: 12th International conference on theorem proving in higher order logics (TPHOLs\u201999), Lecture Notes in Computer Science, vol. 1690, pp. 113\u2013130. Springer, Nice (1999)"},{"key":"9317_CR17","first-page":"217","volume-title":"In: 3rd International conference on formal methods in computer-aided design (FMCAD), Lecture Notes in Computer Science, vol. 1954","author":"J Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of floating point trigonometric functions In: 3rd International conference on formal methods in computer-aided design (FMCAD), Lecture Notes in Computer Science, vol. 1954, pp. 217\u2013233. Springer, Austin (2000)"},{"key":"9317_CR18","unstructured":"IBM: The PowerPC compiler writer\u2019s guide. Warthman Associates (1996)"},{"key":"9317_CR19","first-page":"75","volume-title":"In: 19th international symposium on static analysis, Lecture Notes in Computer Science, vol. 7460","author":"A Ioualalen","year":"2012","unstructured":"Ioualalen, A., Martel, M.: A new abstract domain for the representation of mathematically equivalent expressions In: 19th international symposium on static analysis, Lecture Notes in Computer Science, vol. 7460, pp. 75\u201393. Springer, Berlin Heidelberg New York (2012)"},{"key":"9317_CR20","unstructured":"ISO: International standard ISO\/IEC 9899:2011, Programming languages \u2013 C (2011)"},{"issue":"2","key":"9317_CR21","doi-asserted-by":"crossref","first-page":"75","DOI":"10.5381\/jot.2006.5.2.c8","volume":"5","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T.: Not a number of floating point problems. J. Object Technol. 5(2), 75\u201383 (2006)","journal-title":"J. Object Technol."},{"issue":"7","key":"9317_CR22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9317_CR23","unstructured":"Leroy, X.: The CompCert verified compiler, software and commented proof. Available at http:\/\/compcert.inria.fr\/ (2014)"},{"key":"9317_CR24","first-page":"205","volume-title":"In: 16th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 4421","author":"G Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: Nicola, R.D. (ed.) In: 16th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 4421, pp. 205\u2013219. Springer, Braga (2007)"},{"key":"9317_CR25","unstructured":"Microprocessor Standards Subcommittee: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008 pp. 1\u201358 (2008)"},{"key":"9317_CR26","unstructured":"Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) 7th annual machine intelligence workshop, Machine Intelligence, vol. 7, pp. 51\u201372. Edinburgh University Press (1972)"},{"issue":"3","key":"9317_CR27","doi-asserted-by":"crossref","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. Lang. Syst. 30(3), 1\u201341 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"9317_CR28","first-page":"461","volume":"5","author":"JS Moore","year":"1989","unstructured":"Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461\u2013492 (1989)","journal-title":"J. Autom. Reason."},{"key":"9317_CR29","doi-asserted-by":"crossref","unstructured":"Muller, J.M., Brisebarre, N., de Dinechin, F., Jeannerod, C.P., Lef\u00e8vre, V., Melquiond, G., Revol, N., Stehl\u00e9, D., Torres, S.: Handbook of floating-point arithmetic. Birkh\u00e4user (2010)","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"9317_CR30","unstructured":"Myreen, Magnus O.: Formal verification of machine-code programs. Ph.D. Thesis, University of Cambridge (2008)"},{"key":"9317_CR31","first-page":"314","volume-title":"International conference on certified programs and proofs (CPP), Lecture Notes in Computer Science, vol. 7086","author":"TMT Nguyen","year":"2011","unstructured":"Nguyen, T.M.T., March\u00e9, C.: Hardware-dependent proofs of numerical programs. In: Jouannaud, J.P., Shao, Z. (eds.) International conference on certified programs and proofs (CPP), Lecture Notes in Computer Science, vol. 7086, pp. 314\u2013329. Springer, Berlin Heidelberg New York (2011)"},{"issue":"2","key":"9317_CR32","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/MM.2010.41","volume":"30","author":"J Nickolls","year":"2010","unstructured":"Nickolls, J., Dally, W.: The GPU computing era. IEEE Micro 30(2), 56\u201369 (2010)","journal-title":"IEEE Micro"},{"issue":"1","key":"9317_CR33","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1137\/050645671","volume":"31","author":"S Rump","year":"2008","unstructured":"Rump, S., Ogita, T., Oishi, S.: Accurate floating-point summation Part I: Faithful rounding. SIAM J. Sci. Comput. 31(1), 189\u2013224 (2008)","journal-title":"SIAM J. Sci. Comput."},{"key":"9317_CR34","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"DM Russinoff","year":"1998","unstructured":"Russinoff, D.M.: 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 (1998)","journal-title":"LMS J. Comput. Math."},{"key":"9317_CR35","volume-title":"Floating point computation","author":"PH Sterbenz","year":"1974","unstructured":"Sterbenz, P.H.: Floating point computation. Prentice Hall, Englewood Cliffs (1974)"},{"key":"9317_CR36","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers In: 32nd ACM SIGPLAN conference on programming language design and implementation (PLDI), pp. 283\u2013294. ACM Press (2011)","DOI":"10.1145\/1993498.1993532"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9317-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9317-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9317-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T06:55:19Z","timestamp":1566111319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9317-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,6]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9317"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9317-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,6]]}}}