Abstract
This paper presents a formalization in higher-order logic of a generic algorithm that is used in automated strategies for solving global optimization problems. It is a generalization of numerical branch and bound algorithms that compute the minimum of a function on a given domain by recursively dividing the domain and computing estimates for the range of the function on each sub-domain. The correctness statement of the algorithm has been proved in the Prototype Verification System (PVS) theorem prover. This algorithm can be instantiated with specific functions for performing particular global optimization methods. The correctness of the instantiated algorithms is guaranteed by simple properties that need to be verified on the specific input functions. The use of the generic algorithm is illustrated with an instantiation that yields an automated strategy in PVS for estimating the maximum and minimum values of real-valued functions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 116–131. Springer, Heidelberg (2012)
Crespo, L.G., Muñoz, 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)
Daumas, M., Lester, D., Muñoz, C.: Verified real number calculations: A library for interval arithmetic. IEEE Transactions on Computers 58(2), 1–12 (2009)
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), http://www.cl.cam.ac.uk/jrh13/papers/reflect.dvi.gz+
Lorentz, G.G.: Bernstein Polynomials, 2nd edn. Chelsea Publishing Company, New York (1986)
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–17. Springer, Heidelberg (2008)
Moa, B.: Interval Methods for Global Optimization. PhD thesis, University of Victoria (2007)
Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. Cambridge University Press (2009)
Muñoz, C., Carreño, V., Dowek, G., Butler, R.: Formal verification of conflict detection algorithms. International Journal on Software Tools for Technology Transfer 4(3), 371–380 (2003)
Muñoz, C., Narkawicz, A.: Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization. Journal of Automated Reasoning 51(2), 151–196 (2013), http://dx.doi.org/10.1007/s10817-012-9256-3 , doi:10.1007/s10817-012-9256-3
Neumaier, A.: Complete search in continuous global optimization and constraint satisfaction. Acta Numerica 13, 271–369
Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Ray, S., Nataraj, P.S.: An efficient algorithm for range computation of polynomials using the Bernstein form. Journal of Global Optimization 45, 403–426 (2009)
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–397. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Narkawicz, A., Muñoz, C. (2014). A Formally Verified Generic Branching Algorithm for Global Optimization. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)