Computing Certificates of Members in Archimedean Quadratic Modules in \(\mathbb{A}[X]\) and Certifying the Emptiness in Inconsistent Monogenic Archimedean Quadratic Modules in \(\mathbb{A}[X_1, \dots, X_n]\)
Talk, Thesis Defense, Albuquerque, New Mexico, USA
Polynomials have been found to be a powerful tool over hundreds of years for modeling problems in numerous applications in science, engineering, medicine, and other domains; convex optimization, as an example, has many applications. In the context of formal methods, polynomials arise in modeling in aerospace software and robotics–especially collision avoidance, cyber-physical and hybrid systems, autonomous vehicles and controllers based on neural networks. Optimization of a polynomial function subject to polynomial constraints is investigated in many areas–to mention a few, scheduling, resource allocation, financial systems including option pricing and portfolio optimization, quantum information systems, control and system theory, particularly analysis of dynamical systems such as stability, equilibrium, and more recently, in sophisticated modeling of neurons in deep neural networks and machine learning. Modern SMT solvers and theorem provers often resort to linear approximations of polynomials as a pragmatic solution due to the inherent complexities associated with reasoning about polynomial inequalities.