  We introduce reachability analysis for the formal examination of robots. We
propose a novel identification method, which preserves reachset conformance of
linear systems. We additionally propose a simultaneous identification and
control synthesis scheme to obtain optimal controllers with formal guarantees.
In a case study, we examine the effectiveness of using reachability analysis to
synthesize a state-feedback controller, a velocity observer, and an output
feedback controller.
