Research

We develop algorithms and tools for the synthesis and verification of reactive systems.

Hyperproperties

The central role of information technology in all aspects of our private and professional lives has led to a fundamental change in the type of program properties we care about. Up to now, the focus has been on functional correctness; in the future, requirements that reflect our societal values, like privacy, fairness, and explainability will be far more important. These properties belong to the class of hyperproperties, which represent sets of sets of execution traces and can therefore specify the relationship between different computations of a reactive system. For example, to ensure fairness in a hiring system, we are interested in the hyperproperty that for all pair of executions in which the applicants only differ in sensitive attributes – those that should not be taken into consideration by the hiring system – the final hiring decision is the same.

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; the analysis of the complexity and expressivity of those logics; the construction of algorithms that automatically check if a system satisfies a hyperproperty; the synthesis of systems thats satisfy the desired hyperproperties by construction; and monitoring algorithms that judge the satisfaction of hyperproperties in a running system.

Reactive Synthesis

The grand vision of synthesis is that an engineer analyzes the design objectives that capture what the system should do while the synthesis algorithm decides how the system will meet these objectives. This shifts the burden of writing a correct implementation from the engineer to the synthesis algorithm, while the engineer needs to ensure the correctness of the specification. The synthesis process supports the engineer in identifying competing or contradictory requirements and obtaining an error-free specification from which a correct implementation can be synthesized.

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. For example, explainable synthesis provides explanations for design decisions; knowledge-based synthesis explains the behavior of the system by referring to the evolving knowledge of the individual components.

Runtime Monitoring

Runtime monitoring validates a system against a formal specification at runtime. It is a crucial step in assuring the correct behaviour of cyber-physical systems and asserting their compliance with safety regulations.

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. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides real-time analysis in the form of comprehensive statistics and logical assessments of the system’s health. Every specification is analyzed rigorously before its deployment, eliminating undefined behavior during runtime. This process includes determining the validity of the specification and its memory requirement. Plus, the constant memory guarantee effectively allows the monitor to run indefinitely. RTLola is used by leading avionics experts like the German Aerospace Center.

Neuro-symbolic Formal Methods

The intersection of deep learning and formal methods is a young research area that integrates deep neural networks with rigorous formal reasoning. Applications of deep learning to symbolic domains, such as programming languages, are already adopted but often lack the integration of formal reasoning and logics that are required for analyzing formal correctness.

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 can be described along the following lines (1) Developing methods with both neural and algorithmic components that increase the applicability and reduce the manual effort of formal methods. Practical instances of verification and synthesis problems often follow a particular structure, and similar problems are solved over and over again. Deep neural networks, with their ability to learn rich patterns and to improve from experience, can be utilized in such cases and largely increase efficiency. (2) Bridging formal methods with domains that are inherently difficult to formalize. Formal specifications are the cornerstone of formal methods, but it is often easier and more common to express specifications in natural language. The auto-formalization of specifications with language models emerged as a new paradigm to translate between those domains. (3) Developing a more principled understanding of the relationship between neural and symbolic reasoning mechanisms. To this end, formal reasoning problems provide a testbed rooted in computability, complexity, and comprehensive results on the relationship of problems to study training, generalization abilities, and expressive power of modern deep neural networks.