VERIFICATION OF MULTI-THREADED PROGRAMS AND PARAMETERIZED VERIFICATION.
Many modern IT systems are distributed over different physical locations and are expected to be scalable in parameters such as the number of concurrently running threads or the number of users. Such systems are routinely deployed to handle sensitive information or to control safety-critical processes, for example in cloud computing, industrial control systems or wireless sensor networks. However, the design of distributed systems is highly complex and error-prone, as it must take into account all possible interactions between system components, including hardware or network failures, as well as malicious adversaries. We study the fundamental problem of obtaining correctness guarantees for distributed systems with a large number of components.
Verification of Multi-threaded Programs. To scale verification methods to large values of parameters, such as the number of threads in multi-threaded programs, we research the foundational dependencies between the separate threads of a program with respect to a given goal, such as successful termination. Based on a deep understanding of their interactions, we develop novel verification paradigms that do not directly depend on the number of threads and therefore scale to very large values of this parameter.
Parameterized Verification. We research classes of systems for which correctness guarantees can be given regardless of the number of components or participants. We systematically study the relations between different system models, allowing fundamental insights into the classes of programs they capture, and which of their properties can be automatically determined. We develop application-specific abstractions of arbitrary-size systems, on which we build algorithms that can provide safety and security guarantees regardless of the size of the system.
Distributed and Parameterized Synthesis. In the presence of complex interactions between components, as well as unforeseen failures and adversaries, the desired properties of distributed systems are usually much easier to specify than to implement. Therefore, they are a prime goal for formal synthesis techniques that automatically transform a description of the desired properties in a formal specification language into a distributed system that is correct by construction. We investigate foundations and methods for formal synthesis, including prerequesites for their application as well as new synthesis paradigms that produce high-quality implementations.
