Safety Verification of Iterative Algorithms over Polynomial Vector Fields

Iterative algorithms such as the Newton method or the steepest gradient method appear in real-time software to solve online optimization problems as part of autonomous decision making algorithms. Proving safety and in particular convergence properties of such methods in their generic form is hopeless. However, for a special class of problems over a limited range of inputs and uncertain parameters, such task may become possible. In this paper, we consider applications of the Newton method to polynomial root finding and suggest new methods, based on Lyapunov invariance analysis and sum of squares programming to prove convergence and other performance properties of such algorithms. Generic forms for such Lyapunov invariants are presented and it is shown how the search for the certificates of performance can be formulated as a sum of squares program. The proof methods can be automated and thus integrated within a verification and validation workspace for software verification