  Formal verification has been successfully developed in computer science for
verifying combinatorial classes of models and specifications. In like manner,
formal verification methods have been developed for dynamical systems. However,
the verification of system properties, such as safety, is based on reachability
calculations, which are the sources of insurmountable complexity. This talk
addresses indirect verification methods, which are based on abstracting the
dynamical systems by models of reduced complexity and preserving central
properties of the original systems.
