We present the application of real quantifier elimination to formal
verification and synthesis of continuous and switched dynamical systems.
Through a series of case studies, we show how first-order formulas over the
reals arise when formally analyzing models of complex control systems. Existing
off-the-shelf quantifier elimination procedures are not successful in
eliminating quantifiers from many of our benchmarks. We therefore automatically
combine three established software components: virtual subtitution based
quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition
implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We
use this combination to successfully analyze various models of systems
including adaptive cruise control in automobiles, adaptive flight control
system, and the classical inverted pendulum problem studied in control theory.