Research Group
Finkbeiner
Reactive Systems
We develop methods for the design of systems that are provably safe and secure. Rooted in formal methods and mathematics, our techniques cover the entire software development process from requirements to deployment. We design expressive specification languages (temporal logics, hyperproperties), algorithms for automatic program synthesis and repair (controller synthesis, output-sensitive synthesis), and tools for static verification (MCHyper) and runtime monitoring and enforcement (RTLola). Our research has immediate impact in areas such as distributed, mobile, and autonomous systems and builds foundations that help us understand the digital systems defining tomorrow’s society.
