Logical Analysis of Hybrid Systems
Hybrid systems analysis studies the question "how can we build computerized
controllers for physical systems that are guaranteed to meet their design
goals?" Important application areas include safety-critical systems like
adaptive cruise control technology for cars, auto pilots for aircraft
collision avoidance, control software for mobile robots, and medical devices.
Among other research at Carnegie Mellon University, we develop the logic-based
analysis tool KeYmaera for hybrid systems and cyber-physical systems.
It is based on the theorem prover KeY and combines ideas from model
checking and computer algebra.
Possible topics for masters theses / Phd research range from
theoretical contributions for logic-based analysis techniques over
practical contributions in advancing our Java-based analysis tools to
applied contributions in studying particular systems.
More information on the KeYmaera system:
Applications for financial support may be submitted to interACT
Karlsruhe: Peter H. Schmitt <firstname.lastname@example.org>
CMU: Andre Platzer <email@example.com>