Georg Zetzsche awarded ERC Starting Grant
Georg Zetzsche, head of the MPI-SWS Models of Computation group, has been awarded a 2022 ERC Starting Grant. Over the next five years, his project FINABIS will receive funding of 1.48 million euros for research on "Finite-state abstractions of infinite-state systems." Read more about the FINABIS project below.
In addition, MPI-SWS and University of Saarland alumnus Pramod Bhatotia, who is currently a professor at TU Munich, has also received a 2022 ERC Starting Grant for his project "DOS: A Decentralized Operating System".
...Georg Zetzsche, head of the MPI-SWS Models of Computation group, has been awarded a 2022 ERC Starting Grant. Over the next five years, his project FINABIS will receive funding of 1.48 million euros for research on "Finite-state abstractions of infinite-state systems." Read more about the FINABIS project below.
In addition, MPI-SWS and University of Saarland alumnus Pramod Bhatotia, who is currently a professor at TU Munich, has also received a 2022 ERC Starting Grant for his project "DOS: A Decentralized Operating System".
ERC grants are the most prestigious and the most competitive European-level awards for ground-breaking scientific investigations. This year, less than 14% of all ERC Starting Grant applicants across all scientific disciplines received the award, with only 17 awardees in Computer Science across all of Europe and Israel!
These grants carry substantial research funding -- each winner receives up to 1.5 Million Euros over a period of 5 years to carry out their research. You can find more information about 2022 ERC Starting Grants here: https://erc.europa.eu/news-events/news/starting-grants-2022-call-results
The FINABIS Project
A fundamental question in computing is: What can programs find out algorithmically about other programs? If we want to analyze arbitrary programs, the answer is long known and simple: Essentially nothing. However, in recent decades, we have seen that if we restrict the class of analyzed programs, there is a rich variety of approaches to checking various important properties.
Understanding how to restrict the analyzed programs (while retaining as much expressivity as possible) has gained practical importance in the area of software verification. Here, algorithms for analyzing programs can be used to automatically check their correctness.
The available approaches to analyze programs typically transform a given program into an abstract model of computation. To account for program behaviors for all possible inputs, this usually results in models with infinitely many states. Designing algorithms that can work with such infinite-state systems poses a challenge. For example, we still do not have a clear picture of which types of infinite state spaces permit checking simple safety properties. In formal terms: For which infinite-state systems is reachability decidable?
In the FINABIS project ("Finite-state abstractions of infinite-state systems"), we are studying ways to transform infinite-state systems into finite-state systems that preserve some pertinent aspects of the original system. Understanding such transformations helps in two ways: First, finite-state systems are easier to work with algorithmically. So if our transformation preserves enough of the original system's behavior, we can simply analyze the finite system instead. Second, the specific transformations we study (subword closures and separability problems), and how we study them, are closely connected to understanding the decidability and complexity of reachability and also several other long-standing open problems in theoretical computer science.