loop system, was solved in linear control theory decades ago. This is not true for static output
feedback controller design, which is still an open problem. Here an approach is presented
which handles the existence and design problem using quantifier elimination methods. Our
approach allows the formal verification of arbitrary eigenvalue placement and enables the
construction of controllers which lead to specified dynamic behavior. The design method is …