So-called ‘discrete dynamical systems’ form the basis for key computational challenges in a variety of fields, from program analysis and computer-aided verification to artificial intelligence and theoretical biology. Creating algorithmic solutions to make these systems amenable to automated verification techniques remains a major challenge. Researchers at the Max Planck Institute for Software Systems in Saarbrücken and the French ‘Centre National de la Recherche Scientifique’ are now working on advancing this automated verification approach with substantial funding by the European Research Council.

The interdisciplinary project, titled ‘Dynamical and Arithmetical Model Checking (DynAMiCs)’, is led by the three principal investigators—Professor Joël Ouaknine, Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken; Professor Florian Luca, also MPI-SWS and Stellenbosch University in South Africa; and Professor Valérie Berthé from the French ‘Institut de recherche en informatique fondamentale’ at the ‘Centre National de la Recherche Scientifique (CNRS)’ at the University Paris Cité.

“The paradigm of ‘model checking’ is a powerful method that allows us to automatically verify, with mathematical certainty, whether a system behaves as intended” says Prof. Joël Ouaknine. However, many discrete dynamical systems—systems that change over time following specific rules—cannot currently be verified with the available model-checking approaches.

One of the leading objectives of this new research project is thus to substantially broaden the classes of dynamical systems and properties that can be algorithmically handled via model checking. Specifically, it aims to tackle longstanding mathematical challenges, such as the Skolem Problem, that could lead to breakthroughs in understanding and verifying the behavior of other complex systems.

The Skolem Problem asks if, within a system following specific mathematical rules, a certain state will eventually be reached. Translated to other instances, this question could ask if a computer program will terminate under specific conditions, when an electric vehicle’s battery will fully deplete following a specific driving pattern, or if a manufacturing robot will reach a precise target after following programmed movements. Although seemingly simple, this mathematical problem has remained unsolved and has puzzled mathematicians and computer scientists alike for nearly a century.

Besides the Skolem Problem, the project also addresses additional longstanding mathematical challenges such as the Pisot Conjecture, piecewise-affine map reachability, and the Periodicity Conjecture. Addressing these complex problems demands innovative approaches that integrate insights from multiple areas of mathematics and computer science. “This funding allows us to leverage the interdisciplinary synergies between different fields, bringing together expertise that might not otherwise have come together,” says Florian Luca. The DynAMiCs project unites expertise in algorithmic verification led by Prof. Joël Ouaknine, symbolic dynamics under Prof. Valérie Berthé, and analytic number theory led by Prof. Florian Luca.

The project is funded via a European Research Council (ERC) Synergy Grant totaling 7.5 million euros over six years, with 5 million euros allocated to MPI-SWS. ERC Grants are among the most prestigious research awards globally, with Synergy Grants being especially competitive and offering the highest funding levels. In the current funding round, 548 proposals were submitted, of which only 57 were approved (10.4%).

Further Information:

Press Release by the European Research Council: https://erc.europa.eu/news-events/news/erc-2024-synergy-grants-results

List of Selected Projects: https://erc.europa.eu/sites/default/files/2024-11/erc-2024-syg-results-all-domains.pdf

Scientific Contact:

Professor Joël Ouaknine, PhD Scientific Director at MPI SWS and Coordinating Principal Investigator of DynAMiCs Max Planck Institute for Software Systems, Saarbrücken Tel: +49 (0)681 9303 9701 E-Mail: joel@mpi-sws.org

Editor:

Philipp Zapf-Schramm Max Planck Institute for Informatics Tel: +49 681 9325 5409 E-Mail: pzs@mpi-inf.mpg.de

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.

Adish Singla, head of the MPI-SWS Machine Teaching Research group, has been awarded a 2021 ERC Starting Grant. Over the next five years, his project TOPS will receive funding of 1.5 million euros for research on "Machine-Assisted Teaching for Open-Ended Problem Solving: Foundations and Applications". Read more about the TOPS project below.

ERC grants are the most prestigious and the most competitive European-level awards for ground-breaking scientific investigations. This year, less than 10% of all ERC Starting Grant applicants across all scientific disciplines received the award, with only 23 awardees in Computer Science across all of Europe! You can find more information about ERC Starting Grants awarded this year at https://erc.europa.eu/news/StG-recipients-2021.

The TOPS Project

Computational thinking and problem solving skills are essential for everyone in the 21st century, both for students to excel in STEM+Computing fields and for adults to thrive in the digital economy. Consequently, educators are putting increasing emphasis on pedagogical tasks in open-ended domains such as programming, conceptual puzzles, and virtual reality environments.

When learning to solve such open-ended tasks by themselves, people often struggle. The difficulties are embodied in the very nature of tasks being open-ended: (a) underspecified (multiple solutions of variable quality), (b) conceptual (no well-defined procedure), (c) sequential (series of interdependent steps needed), and (d) exploratory (multiple pathways to reach a solution). These struggling learners can benefit from individualized assistance, for instance, by receiving personalized curriculum across tasks or feedback within a task. Unfortunately, human tutoring resources are scarce, and receiving individualized human-assistance is rather a privilege. Technology empowered by artificial intelligence has the potential to tackle this scarcity challenge by providing scalable and automated machine-assisted teaching. However, the state-of-the-art technology is limited: it is designed for well-defined procedural learning, but not for open-ended conceptual problem solving.

The TOPS project will develop next-generation technology for machine-assisted teaching in open-ended domains. We will design novel algorithms for assisting the learner by bridging reinforcement learning, imitation learning, cognitive science, and symbolic reasoning. Our theoretical foundations will be based on a computational framework that models the learner as a reinforcement learning agent who gains mastery with the assistance of an automated teacher. In addition to providing solid foundations, we will demonstrate the performance of our techniques in a wide range of pedagogical applications.

Viktor Vafeiadis, head of the MPI-SWS Software Analysis and Verification group, has been awarded an ERC Consolidator Grant. Over the next five years, his project "PERSIST: A Semantic Foundation for Persistent Programming" will receive almost 2 million euros, which will allow the group to develop rigorous formal foundations for programs interacting with non-volatile memory. Read more about the PERSIST project below.

One of the other recipients of an ERC Consolidator Grant this year is an MPI alumnus: Neel Krishnaswami was an MPI-SWS postdoc with Derek Dreyer, and he is currently a faculty member at Cambridge.

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 Consolidator Grant applicants across all scientific disciplines received the award, with only 15 awardees in Computer Science across all of Europe! The ERC Consolidator Grant offers funding for researchers with 7 to 12 years of experience after achieving a PhD. You can find more information about ERC Consolidator Grants awarded this year at https://erc.europa.eu/news/CoG-recipients-2020.

The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, across all research areas. Talented researchers from all over the world can receive funding for excellent research in Europe.

The PERSIST Project

Non-volatile memory (NVM) is an emerging technology that provides orders of magnitude faster access to persistent storage (which preserves its contents after a crash or a power failure) than hard disks.  As such, it is expected to radically change how modern applications manage storage, moving away from traditional block-structured file systems to in-memory persistent data structures.

The problem with NVM, however, is that its programming model is standing on very shaky foundations. The persistency semantics of the mainstream architectures is unclear and full of counterintuitive behaviours, which makes writing correct NVM programs a very challenging task.

The project's goal is to develop a solid mathematical basis for determining the semantics of NVM programs and for reasoning about their correctness. More specifically, the plan is to produce:

• Formal persistency models for mainstream hardware architectures,
• Formal persistency models for mainstream programming languages,
• Firmly-grounded higher-level abstractions to ease persistent programming, and
• Effective testing and verification techniques for persistent programs (e.g., program logics and model checking).

Manuel Gomez-Rodriguez, head of the MPI-SWS Human-Centric Machine Learning group, has been awarded an ERC Starting Grant. Over the next five years, his project "Human-Centric Machine Learning" will receive 1.49 million euros, which will allow the group to develop the foundations of human-centric machine learning.

In the most recent round for Starting Grants, over 3300 research proposals were submitted to the ERC. The sole selection criterion is scientific excellence. This year, less than 14% of all ERC Starting Grant applicants across all scientific disciplines received the award, with only 20 awardees in Computer Science across all of Europe!

Summary of the HumanML project proposal

With the advent of mass-scale digitization of information and virtually limitless computational power, an increasing number of social, information and cyber-physical systems evaluate, support or even replace human decisions using machine learning models and algorithms. Machine learning models and algorithms have been traditionally designed to take decisions autonomously, without human intervention, on the basis of passively collected data. However, in most social, information and cyber-physical systems, algorithmic and human decisions feed on and influence each other. As these decisions become more consequential to individuals and society, machine learning models and algorithms have been blamed for playing a major role in an increasing number of missteps, from discriminating against minorities, causing car accidents and increasing polarization to misleading people in social media.

In this project, we will develop human-centric machine learning models and algorithms for evaluating, supporting and enhancing decision-making processes where algorithmic and human decisions feed on and influence each other. These models and algorithms will account for the feedback loop between algorithmic and human decisions, which currently perpetuates or even amplifies biases and inequalities, and they will learn to operate under different automation levels. Moreover, they will anticipate how individuals will react to their algorithmic decisions, often strategically, to receive beneficial decisions and they will provide actionable insights about their algorithmic decisions. Finally, we will perform observational and interventional experiments as well as realistic simulations to evaluate their effectiveness in a wide range of applications, from content moderation, recidivism prediction, and credit scoring to medical diagnosis and autonomous driving.

The TOROS project, supported by an ERC Starting Grant, has officially started. The project targets the challenge of implementing safety-critical cyber-physical systems on commodity multicore processors such that their temporal correctness can be certified in a formal, trustworthy manner.

Specifically, the TOROS project aims to design a new theory-oriented RTOS that by construction ensures that the temporal behavior of any workload can be analyzed (regardless of whether an application developer is aware of the relevant scheduling theory), develop a matching novel timing analysis for below-worst-case provisioning with analytically sound safety margins that yields meaningful probabilistic response-time guarantees, and plans to mechanize and verify all supporting scheduling theory with the Coq proof assistant using the Prosa framework.

See the project homepage for further details. For inquiries, contact Björn Brandenburg (toros@mpi-sws.org).

Krishna Gummadi, head of the MPI-SWS Networked Systems group, has been awarded an ERC Advanced Grant. Over the next five years, his project "Foundations of Fair Social Computing" will receive 2.49 million euros, which will allow the group to develop the foundations for fair social computing in the future.

In the most recent round for Advanced Grants, a total of 2,167 research proposals were submitted to the ERC out of which merely 12% were selected for funding. The sole selection criterion is scientific excellence.

Summary of the Fair Social Computing project proposal

Social computing represents a societal-scale symbiosis of humans and computational systems, where humans interact via and with computers, actively providing inputs to influence---and in turn being influenced by---the outputs of the computations. Social computations impact all aspects of our social lives, from what news we get to see and who we meet to what goods and services are offered at what price and how our creditworthiness and welfare benefits are assessed. Given the pervasiveness and impact of social computations, it is imperative that social computations be fair, i.e., perceived as just by the participants subject to the computation. The case for fair computations in democratic societies is self-evident: when computations are deemed unjust, their outcomes will be rejected and they will eventually lose their participants.

Recently, however, several concerns have been raised about the unfairness of social computations pervading our lives, including

1. the existence of implicit biases in online search and recommendations,
2. the potential for discrimination in machine learning based predictive analytics, and
3. a lack of transparency in algorithmic decision making, with systems providing little to no information about which sensitive user data they use or how they use them.

Given these concerns, we need reliable ways to assess and ensure the fairness of social computations. However, it is currently not clear how to determine whether a social computation is fair, how we can compare the fairness of two alternative computations, how to adjust a computational method to make it more fair, or how to construct a fair method by design. This project will tackle these challenges in turn. We propose a set of comprehensive fairness principles, and will show how to apply them to social computations. In particular, we will operationalize fairness, so that it can be measured from empirical observations. We will show how to characterize which fairness criteria are satisfied by a deployed computational system. Finally, we will show how to synthesize non-discriminatory computations, i.e., how to learn an algorithm from training data that satisfies a given fairness principle.

Derek Dreyer, head of the MPI-SWS Foundations of Programming group, has been awarded an ERC Consolidator Grant. Over the next five years, his project "RustBelt: Logical Foundations for the Future of Safe Systems Programming" will receive almost 2 million euros, which will allow the group to develop rigorous formal foundations for the Rust programming language.

The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, across all research areas. Talented researchers from all over the world can receive funding for excellent research in Europe. The ERC Consolidator Grant offers funding for researchers with 7 to 12 years of experience after achieving a PhD.

The RustBelt Project

A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.

Rust is a new language developed at Mozilla Research that marries together the low-level flexibility of modern C++ with a strong "ownership-based" type system guaranteeing type safety, memory safety, and data race freedom. As such, Rust has the potential to revolutionize systems programming, making it possible to build software systems that are safe by construction, without having to give up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art.

In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of "unsafe" code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems.

More

MPI-SWS directors Peter Druschel and Rupak Majumdar, along with Gerhard Weikum (Scientific Director at the MPI for Informatics) and Michael Backes (MPI-SWS Fellow and Professor at Saarland University), have jointly been awarded the prestigious ERC Synergy Grant.

Over the next six years their project "imPACT: Privacy, Accountability, Compliance, and Trust in Tomorrow's Internet" will receive almost 10 million euros, which will allow them to explore how to protect users against eavesdropping and fraud on the Internet without restricting trade, freedom of expression or access to information.

MPI-SWS fellow Michael Backes has been honored as a recipient of the ERC Starting Grant 2009. Michael was also recently selected by the editors of Technology Review as one of the 35 young innovators under the age of 35 whose work they found most exciting.

The ERC Starting Grant was established in 2007 by the European Research Council to support up-and-coming research leaders in Europe. Recipients are selected based upon "outstanding track-record of early achievements appropriate to their research field and career stage."

Michael's 2009 Young Innovator award is based on his work proving that Internet security protocols can really be trusted. Software designed by Backes' group can prove in less than a second whether an Internet protocol is truly secure.

Michael received his Ph.D. from Saarland University in 2002. He was a Research Staff Member at the IBM Zurich Research laboratory before accepting his current position as a professor at Saarland University in 2006. He was named a fellow of the Max-Planck Institute for Software Systems in 2007.