We propose a methodology for the automatic verification of safety properties
of controllers based on dynamical systems, such as those typically used in
avionics. In particular, our focus is on proving stability properties of
software implementing linear and some non-linear controllers. We develop an
abstract interpretation framework that follows closely the Lyapunov methods
used in proofs at the model level and describe the corresponding abstract
domains, which for linear systems consist of ellipsoidal constraints.