{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:00Z","timestamp":1776305220442,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642182747","type":"print"},{"value":"9783642182754","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_17","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T00:06:38Z","timestamp":1295222798000},"page":"232-247","source":"Crossref","is-referenced-by-count":74,"title":["Static Analysis of Finite Precision Computations"],"prefix":"10.1007","author":[{"given":"Eric","family":"Goubault","sequence":"first","affiliation":[]},{"given":"Sylvie","family":"Putot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.-C.: Formal Verification of Floating-Point Programs. In: 18th IEEE International Symposium on Computer Arithmetic (June 2007)","DOI":"10.1109\/ARITH.2007.20"},{"key":"17_CR2","unstructured":"Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SEBGRAPI 1993 (1993)"},{"key":"17_CR3","unstructured":"Conquet, E., Cousot, P., Cousot, R., Goubault, E., Ghorbal, K., Lesens, D., Putot, S., Turin, M.: Space software validation using abstract interpretation. In: Proceedings of DASIA (2009)"},{"key":"17_CR4","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, pp. 106\u2013130 (1976)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Formal Methods for Industrial Critical Systems","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: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 53\u201369. Springer, Heidelberg (2009)"},{"key":"17_CR6","unstructured":"Zimmerman, P., et al.: The MPFR library, \n                  \n                    http:\/\/www.mpfr.org\/"},{"key":"17_CR7","unstructured":"IEEE 754 Standard for Binary Floating-Point\u00a0Arithmetic, revision (2008), \n                  \n                    http:\/\/ieeexplore.ieee.org\/servlet\/opac?punumber=4610933"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/978-3-642-02658-4_47","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2009","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 627\u2013633. Springer, Heidelberg (2009)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-14295-6_22","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2010","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 212\u2013226. Springer, Heidelberg (2010)"},{"issue":"1","key":"17_CR10","doi-asserted-by":"publisher","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.\u00a023(1), 5\u201348 (1991)","journal-title":"ACM Comput. Surv."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-47764-0_14","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2001","unstructured":"Goubault, \u00c9.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 234\u2013259. Springer, Heidelberg (2001)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45927-8_15","volume-title":"Programming Languages and Systems","author":"\u00c9. Goubault","year":"2002","unstructured":"Goubault, \u00c9., Martel, M., Putot, S.: Asserting the precision of floating-point computations: A simple abstract interpreter. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 209\u2013212. Springer, Heidelberg (2002)"},{"key":"17_CR13","unstructured":"Goubault, \u00c9., Putot, S.: Weakly relational domains for the analysis of floating-point computations. Presented at NSAD (2005)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2006","unstructured":"Goubault, \u00c9., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 18\u201334. Springer, Heidelberg (2006)"},{"key":"17_CR15","unstructured":"Goubault, E., Putot, S.: Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR, abs\/0807.2961 (2008)"},{"key":"17_CR16","unstructured":"Goubault, E., Putot, S.: A zonotopic framework for functional abstractions. CoRR, abs\/0910.1763 (2009), \n                  \n                    http:\/\/arxiv.org\/abs\/0910.1763"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-79707-4_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"\u00c9. Goubault","year":"2008","unstructured":"Goubault, \u00c9., Putot, S., Baufreton, P., Gassino, J.: Static analysis of the accuracy in control systems: Principles and experiments. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 3\u201320. Springer, Heidelberg (2008)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-45927-8_14","volume-title":"Programming Languages and Systems","author":"M. Martel","year":"2002","unstructured":"Martel, M.: Propagation of roundoff errors in finite precision computations: A semantics approach. In: Le M\u00e9tayer, D. (ed.) ESOP 2002. LNCS, vol.\u00a02305, pp. 194\u2013208. Springer, Heidelberg (2002)"},{"key":"17_CR19","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718140","volume-title":"The Lanczos and Conjugate Gradient Algorithm; from theory to finite precision computation","author":"G. Meurant","year":"2006","unstructured":"Meurant, G.: The Lanczos and Conjugate Gradient Algorithm; from theory to finite precision computation. SIAM, Philadelphia (2006)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Min\u00e9","year":"2005","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 348\u2013363. Springer, Heidelberg (2005)"},{"issue":"3","key":"17_CR22","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. Lang. Syst.\u00a030(3), 1\u201341 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR23","unstructured":"Muller, J.-M.: Arithm\u00e9tique des Ordinateurs. Masson (1989)"},{"key":"17_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"J.-M. Muller","year":"2010","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, Boston (2010)"},{"key":"17_CR25","unstructured":"APRON Project. Numerical abstract domain library (2007), \n                  \n                    http:\/\/apron.cri.ensmp.fr"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-24738-8_18","volume-title":"Numerical Software with Result Verification","author":"S. Putot","year":"2004","unstructured":"Putot, S., Goubault, \u00c9., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol.\u00a02991, pp. 306\u2013313. Springer, Heidelberg (2004)"},{"key":"17_CR27","unstructured":"Skeel, R.: Roundoff error and the patriot missile. SIAM News (1992)"},{"key":"17_CR28","volume-title":"Floating point computation","author":"P.H. Sterbenz","year":"1974","unstructured":"Sterbenz, P.H.: Floating point computation. Prentice-Hall, Englewood Cliffs (1974)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18275-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T19:24:31Z","timestamp":1553369071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}