Seminars

Formally Solving Nonlinear Arithmetic Problems With Bernstein Polynomi

Cesar A. Munoz
NASA-Langley Research Center, Hampton, VA

12/12/2011, 2pm, GHC-6501

Abstract

Many engineering problems require determining whether, given bounds on the variables of a multivariate polynomial, the output values of the polynomial always fall within a particular range. Such problems are called "polynomial global optimization problems". This talk presents formal definitions of algorithms based on Bernstein polynomials that can be used to automatically and formally solve polynomial global optimization problems. Solving such problems has typically been accomplished in theorem provers such as PVS, Coq, HOL Light, MetiTarski, and RAHD by quantifier elimination procedures. However, these methods do not scale well to problems with many variables.

The formalization presented in this talk enables a practical representation of multivariate Bernstein polynomials in a higher-order logic. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a multivariate polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies and prototype tools for formally and automatically solving simply quantified multivariate polynomial inequalities and other polynomial global optimization problems.

Biography

César Muñoz earned an Engineering and a Master degree in Computer Science from the Universidad de los Andes (Bogotá), and a M.Sc. and Ph.D. in Computer Science from the University of Paris 7 (Paris). After completing his Ph.D., he spent one and a half years as an International Fellow in the Computer Science Laboratory at SRI International in Menlo Park. In 1999, he joined the Formal Methods group at ICASE - NASA Langley. From 2003 to 2008, he worked for the National Institute of Aerospace at Langley Research Center, where he led the NIA Formal Methods group. Since 2009, César Muñoz is a Research Computer Scientist at NASA. Currently, César Muñoz works on the development of formal methods technology for NASA's Next Generation of Air Traffic Systems (NextGen), Validation and Verification of Flight Critical Systems (VVFCCS), and Unmanned Aircraft Systems Integration in the National Airspace (UAS in the NASA) projects.