Research
Hyperproperties
Hyperproperties capture system requirements that relate multiple execution traces at once.
Our research sets out to develop a unified theory for general hyperproperties. This includes the development of new logics that can capture rich classes of hyperproperties, including information flow policies, causality, and algorithmic fairness.
Reactive Synthesis
Reactive synthesis automatically constructs a system that continuously responds to its environment while guaranteeing that a formal specification is always satisfied.
Our research targets the synthesis of distributed systems with multiple components and cyber-physical systems that combine discrete controllers with models of the dynamics of their physical environment. We specifically aim for synthesis techniques that produce understandable, trustworthy solutions.
Runtime Monitoring
Runtime monitoring observes a system during execution to detect property violations, security breaches, or anomalous behavior as they occur.
In our research, we develop formal specification languages for monitoring, algorithms for the synthesis of resource-efficient and correct-by-construction monitors, and domain-specific solutions for autonomous cyber-physical systems. At the center of our research is the stream-based runtime monitoring framework RTLola.
Neuro-symbolic Formal Methods
Neuro-symbolic computing integrates learning-based neural methods with symbolic reasoning to create AI systems that are both data-driven and logically grounded.
In our research, we use deep learning methods to facilitate the formalization, formal verification and synthesis of software and hardware systems. The goals of this research include developing methods with both neural and algorithmic components that increase the applicability and reduce the manual effort of formal methods.
Grants & Projects
-
PreCePT
2024 – 2026Precise Monitoring of Cyber-Physical Technology under Uncertainty
- 2024
-
HYPER
2022 – 2027Logics and Algorithms for a Unified Theory of HyperpropertiesERC Advanced Grant
- 2022
-
Knowledge-based Synthesis
2020 – 2023GIF Research Grant Regular Program
-
VoloSTreAM
2020 – 2023Reliable runtime monitoring by means of traceable status analysis for highly critical eVOTL operation
- 2020
-
CPEC
2019 – 2026Center for Perspicuous Computing – Distributed Knowledge and Information FlowTransregional Collaborative Research Centre
- 2019
-
OSARES
2016 – 2021Output-Sensitive Algorithms for Reactive SynthesisERC Consolidator Grant
- 2016