Research
Current and past research project at the KIT.
About the Alexander von Humboldt Professorship.
The Alexander von Humboldt Professorship, Germany’s most highly endowed international research award, is endowed with up to five million euros. With this award, the Alexander von Humboldt Foundation honors internationally leading researchers of all disciplines who have previously worked abroad. They are expected to conduct forward-looking research at German universities in the long term. The money is earmarked for the first five years of research in Germany. The award is financed by the German Federal Ministry of Education and Research. The Humboldt Professorship enables German universities to attract top international researchers and to strengthen their own profile in global competition. The award is linked to an obligation to offer the new Humboldt Professors long-term prospects for their research in Germany. Additional funding for Humboldt professorships in artificial intelligence will be available through 2024; the holders of these professorships can also investigate the social, legal or ethical aspects of artificial intelligence.
Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and therefore should strive for nothing but the highest safety standards - mathematical correctness proof. Proofs for such cyber-physical systems can be constructed with the KeYmaera X prover. As a hybrid systems theorem prover, KeYmaera X analyzes the control program and the physical behavior of the controlled system together in differential dynamic logic.
KeYmaera X features a minimal core of just about 2000 lines of code that isolates all soundness-critical reasoning. Such a small and simple prover core makes it much easier to trust verification results. Pre-defined and custom tactics built on top of the core drive automated proof search. KeYmaera X comes with a web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity. Besides hybrid systems, KeYmaera X also supports the verification of hybrid games in differential game logic.
The logic of autonomous dynamical systems group is part of the Helmholtz Pilot Program Core-Informatics at KIT (KiKIT).
Logical Refinement Reasoning for Dynamical Systems
System properties and system relations are the two fundamental
judgments about dynamical systems (or programs). This project aims
at uniting both styles of reasoning in a single logic implementable
in a theorem prover microkernel. This makes it possible to
implement the first verification tool supporting mix and match
reasoning about dynamical systems.