The seminar activities are partially supported by the National Science Foundation.

Talks of the Spring 2019 semester are available here.

Talks of the Fall 2018 semester are available here.

Talks of the Spring 2018 semester are available here.

For earlier seminars, see the old webpage.

Slides

Video

Video

Video

In part (i), we study the power and limitations of sum of squares optimization and semialgebraic Lyapunov functions for proving asymptotic stability of polynomial dynamical systems. We give the first example of a globally asymptotically stable polynomial vector field with rational coefficients that does not admit a polynomial (or even analytic) Lyapunov function in any neighborhood of the origin. We show, however, that if the polynomial vector field is homogeneous, then its asymptotic stability is equivalent to existence of a rational Lyapunov function whose inequalities have sum of squares proofs. This statement generalizes the classical result in control on the equivalence between asymptotic stability of linear systems and existence of a quadratic Lyapunov function satisfying a certain linear matrix inequality.

In part (ii), we study a new class of optimization problems that have constraints imposed by trajectories of a dynamical system. As a concrete example, we consider the problem of minimizing a linear function over the set of points that remain in a given polyhedron under the repeated action of a linear, or a switched linear, dynamical system. We present a hierarchy of linear and semidefinite programs that respectively lower and upper bound the optimal value of such problems to arbitrary accuracy. We show that on problem instances where the spectral radius of the linear system is bounded above by some constant less than one, our hierarchies find an optimal solution and a certificate of optimality in polynomial time. Joint work with Bachir El Khadir (part (i)) and with Oktay Gunluk (part (ii)).

Video

Slides

Video

Slides

Video

Slides

Video

This is joint work with Gareth Jones, Olivier Le Gal, and Tamara Servi.

Slides

Video

Slides

Video

Slides

Video

I will talk about formalization of mathematics and my formalization of
ordinary differential equations in the Isabelle/HOL theorem prover.
This underpins the formal verification of the computer-assisted part of
Tucker's proof of Smale's 14th problem, a proof that relies on numerical
bounds to certify chaos for the Lorenz system of ordinary differential
equations.

Slides

Video

Slides

Video

Video

Slides

Video