For many high (and infinite) dimensional dynamical systems it is not feasible to explore the dynamics in the entire phase space. Instead, one needs to focus on a set of special solutions that act as organizing centers (for example because they form the skeleton of the attractor). To single out these solutions a functional analytic approach to rigorous dynamics is being developed to find, for example, fixed points, periodic orbits and connecting orbits between those.

This tutorial will provide an introduction to the ingredients that are required for rigorous verification of solutions of nonlinear dynamical systems. In a nutshell, verification methods are mathematical theorems formulated in such a way that the assumptions can be rigorously verified on a computer. Indeed, it requires an a priori setup that allows analysis and numerics to go hand in hand: the choice of function spaces, the choice of the basis functions/elements and Galerkin projections, the analytic estimates, and the computational parameters must all work together to bound the errors due to approximation, rounding and truncation sufficiently tightly for the verification proof to go through.

The tutorial will cover the underlying theory, computational aspects, as well as practical applications of the methods. In particular, the following topics will be discussed:

1. Functional analytic setup of a computation-friendly framework.
2. Rigorous computation of periodic orbits and their stability analysis.
3. Rigorous computation of (un)stable manifolds and connecting orbits.
4. Parameter continuation and bifurcations.

Hands-on discussions of code will be an integral part of the tutorial.