{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:52Z","timestamp":1746745492473,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319221014"},{"type":"electronic","value":"9783319221021"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_20","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"294-309","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Affine Arithmetic and Applications to Real-Number Proving"],"prefix":"10.1007","author":[{"given":"Mariano M.","family":"Moscato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew P.","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"issue":"4","key":"20_CR1","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-012-9255-4","volume":"50","author":"S Boldo","year":"2013","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: A comprehensive mechanized proof of a C program. J. Autom. Reasoning 50(4), 423\u2013456 (2013). http:\/\/hal.inria.fr\/hal-00649240\/en\/","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"20_CR2","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/j.camwa.2014.06.004","volume":"68","author":"S Boldo","year":"2014","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Trusting computations: a mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3), 325\u2013352 (2014). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0898122114002636","journal-title":"Comput. Math. Appl."},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/s11786-011-0099-9","volume":"5","author":"S Boldo","year":"2011","unstructured":"Boldo, S., March\u00e9, C.: Formal verification of numerical programs: From C annotated programs to mechanical proofs. Math. Comput. Sci. 5, 377\u2013393 (2011). http:\/\/dx.doi.org\/10.1007\/s11786-011-0099-9","journal-title":"Math. Comput. Sci."},{"issue":"2","key":"20_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput. 58(2), 1\u201312 (2009)","journal-title":"IEEE Trans. Comput."},{"issue":"1\u20134","key":"20_CR5","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/B:NUMA.0000049462.70970.b6","volume":"37","author":"LH de Figueiredo","year":"2004","unstructured":"de Figueiredo, L.H., Stolfi, J.: Affine arithmetic: Concepts and applications. Numer. Algorithms 37(1\u20134), 147\u2013158 (2004)","journal-title":"Numer. Algorithms"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-73445-1_13","volume-title":"Logic, Language, Information and Computation","author":"AL Galdino","year":"2007","unstructured":"Galdino, A.L., Mu\u00f1oz, C., Ayala-Rinc\u00f3n, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 177\u2013188. Springer, Heidelberg (2007)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-38088-4_31","volume-title":"NASA Formal Methods","author":"AE Goodloe","year":"2013","unstructured":"Goodloe, A.E., Mu\u00f1oz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: From real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441\u2013446. Springer, Heidelberg (2013)"},{"key":"20_CR8","unstructured":"Hales, T., Adams, M., Bauer, G., Tat Dang, D., Harrison, J., Le Hoang, T., Kaliszyk, C., Magron, V., McLaughlin, S., Tat Nguyen, T., Quang Nguyen, T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Hoai Thi Ta, A., Tran, T.N., Thi Trieu, D., Urban, J., Khac Vu, K., Zumkeller, R.: A formal proof of the Kepler conjecture. ArXiv e-prints, January 2015"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-06200-6_9","volume-title":"NASA Formal Methods","author":"F Immler","year":"2014","unstructured":"Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113\u2013127. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/978-3-319-06200-6"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Immler, F.: A verified algorithm for geometric zonotope\/hyperplane intersection. In: Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP), pp. 129\u2013136. ACM, New York (2015). http:\/\/doi.acm.org\/10.1145\/2676724.2693164","DOI":"10.1145\/2676724.2693164"},{"key":"20_CR11","first-page":"114","volume":"16","author":"S Kiel","year":"2012","unstructured":"Kiel, S.: Yalaa: Yet another library for affine arithmetic. Reliable Comput. 16, 114\u2013129 (2012)","journal-title":"Reliable Comput."},{"key":"20_CR12","volume-title":"Bernstein Polynomials","author":"GG Lorentz","year":"1986","unstructured":"Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York (1986)","edition":"2"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-71070-7_2","volume-title":"Automated Reasoning","author":"G Melquiond","year":"2008","unstructured":"Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 2\u201317. Springer, Heidelberg (2008)"},{"key":"20_CR14","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717716","volume-title":"Introduction to Interval Analysis","author":"RE Moore","year":"2009","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM, Philadelphia (2009)"},{"key":"20_CR15","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Contractor Report NASA\/CR-2003-212418, NASA, Langley Research Center, Hampton VA 23681\u20132199, USA (2003)"},{"issue":"3","key":"20_CR16","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/s10009-002-0084-3","volume":"4","author":"C Mu\u00f1oz","year":"2003","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G., Butler, R.: Formal verification of conflict detection algorithms. Int. J. Softw. Tools Technol. Transf. 4(3), 371\u2013380 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"20_CR17","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. J. Autom. Reasoning 51(2), 151\u2013196 (2013). http:\/\/dx.doi.org\/10.1007\/s10817-012-9256-3","journal-title":"J. Autom. Reasoning"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-54108-7_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Narkawicz","year":"2014","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 326\u2013343. Springer, Heidelberg (2014)"},{"issue":"1\u20132","key":"20_CR19","doi-asserted-by":"publisher","first-page":"1039","DOI":"10.1016\/j.scico.2011.07.002","volume":"77","author":"A Narkawicz","year":"2012","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dowek, G.: Provably correct conflict prevention bands algorithms. Sci. Comput. Program. 77(1\u20132), 1039\u20131057 (2012). http:\/\/dx.doi.org\/10.1016\/j.scico.2011.07.002","journal-title":"Sci. Comput. Program."},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verificationsystem. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-38088-4_26","volume-title":"NASA Formal Methods","author":"A Solovyev","year":"2013","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383\u2013397. Springer, Heidelberg (2013)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-22673-1_9","volume-title":"Intelligent Computer Mathematics","author":"A Solovyev","year":"2011","unstructured":"Solovyev, A., Hales, T.C.: Efficient formal verification of bounds of linear programs. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 123\u2013132. Springer, Heidelberg (2011)"},{"key":"20_CR23","unstructured":"Stolfi, J., Figueiredo, L.H.D.: Self-validated numerical methods and applications (1997)"},{"issue":"2","key":"20_CR24","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1145\/317275.317286","volume":"25","author":"J Verschelde","year":"1999","unstructured":"Verschelde, J.: Algorithm 795: PHCpack: A general-purpose solver for polynomial systems by homotopy continuation. ACM Trans. Math. Softw. 25(2), 251\u2013276 (1999)","journal-title":"ACM Trans. Math. Softw."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T11:24:57Z","timestamp":1676028297000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}