{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:40Z","timestamp":1746745480816,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642541070"},{"type":"electronic","value":"9783642541087"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_17","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T05:09:36Z","timestamp":1389762576000},"page":"326-343","source":"Crossref","is-referenced-by-count":24,"title":["A Formally Verified Generic Branching Algorithm for Global Optimization"],"prefix":"10.1007","author":[{"given":"Anthony","family":"Narkawicz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-32759-9_12","volume-title":"FM 2012: Formal Methods","author":"M. Carlier","year":"2012","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 116\u2013131. Springer, Heidelberg (2012)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Crespo, L.G., Mu\u00f1oz, C.A., Narkawicz, A.J., Kenny, S.P., Giesy, D.P.: Uncertainty analysis via failure domain characterization: Polynomial requirement functions. In: Proceedings of European Safety and Reliability Conference, Troyes, France (September 2011)","DOI":"10.1201\/b11433-162"},{"issue":"2","key":"17_CR3","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 Transactions on Computers\u00a058(2), 1\u201312 (2009)","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR4","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), \n                  \n                    http:\/\/www.cl.cam.ac.uk\/jrh13\/papers\/reflect.dvi.gz+"},{"key":"17_CR5","volume-title":"Bernstein Polynomials","author":"G.G. Lorentz","year":"1986","unstructured":"Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York (1986)","edition":"2"},{"key":"17_CR6","series-title":"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.\u00a05195, pp. 2\u201317. Springer, Heidelberg (2008)"},{"key":"17_CR7","unstructured":"Moa, B.: Interval Methods for Global Optimization. PhD thesis, University of Victoria (2007)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. Cambridge University Press (2009)","DOI":"10.1137\/1.9780898717716"},{"issue":"3","key":"17_CR9","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. International Journal on Software Tools for Technology Transfer\u00a04(3), 371\u2013380 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"17_CR10","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. Journal of Automated Reasoning\u00a051(2), 151\u2013196 (2013), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/s10817-012-9256-3\n                  \n                  \n                , doi:10.1007\/s10817-012-9256-3","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Neumaier, A.: Complete search in continuous global optimization and constraint satisfaction. Acta Numerica\u00a013, 271\u2013369","DOI":"10.1017\/S0962492904000194"},{"key":"17_CR12","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 verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s10898-008-9382-y","volume":"45","author":"S. Ray","year":"2009","unstructured":"Ray, S., Nataraj, P.S.: An efficient algorithm for range computation of polynomials using the Bernstein form. Journal of Global Optimization\u00a045, 403\u2013426 (2009)","journal-title":"Journal of Global Optimization"},{"key":"17_CR14","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.\u00a07871, pp. 383\u2013397. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T23:06:53Z","timestamp":1558825613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}