A hybrid system is a dynamical system that exhibits both continous
and discrete behavior, i.e. a system that can both flow (described by
differential equations) and jump (described by difference equations).
Hybrid systems are widely used to model physical systems that are
applied in safety-critical domains such as trains, aircrafts or plants.
The verification of their correctness is therefore of essential
importance. A very prominent example of such a correctness property is
stability.
Classical notions of stability refer to a single equilibrium point,
which is often inadequate for expressing the correctness properties of
hybrid systems. For example, if we consider a heating system, where the
temperature is specified by upper and lower bounds, such an equilibrium
point does not even exist. In this thesis we introduce a new notion of
stability that refers to a region instead of equilibrium points. We give
a method for verifying region stability of hybrid systems., and we
present a tool that we apply to solve a number of challenging
verification problems. The scalability of our approach originates
directly from the use of abstraction techniques.