Manuel Gomez-Rodriguez, head of the MPI-SWS Human-Centric Machine Learning group, has been awarded an ERC Consolidator Grant for his project "Counterfact: Counterfactuals in Minds and Machines." This project will receive circa 2 million euros over a period of 5 years, starting directly after Manuel's ERC Starting Grant project on "Human-Centered Machine Learning" wraps up next year.

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

Summary of the Counterfact project proposal

Reasoning about what might have been, about alternatives to our own pasts, is a landmark of human intelligence. This type of reasoning, called counterfactual reasoning, is often evaluative, specifying alternatives that are in some sense better or worse than our past reality, and has been shown to play a significant role in the ability that humans have to learn from limited past experience and improve their decision making skills over time. In recent years, there has increasing excitement about the potential of machine learning models and algorithms to support human decision making in a variety of high-stakes domains such as medicine, education
or science. However, these models and algorithms have been traditionally unable to perform, nor benefit from, counterfactual reasoning. In this project, our goal is to bridge this gap.

We will develop machine learning models and algorithms for automated decision support that are able to perform and benefit from counterfactual reasoning in multiple ways. For example, they will perform counterfactual reasoning about human behavior in order to anticipate how humans incorporate algorithmic advice into their decisions. This will enable a new generation of decision support systems that can only increase and never decrease the average quality of human decisions. Moreover, they will use the structural similarities and shared properties across different counterfactual decision making scenarios to significantly reduce their computational and data requirements. In addition, these models and algorithms will also help humans learn from their own past decisions by identifying alternative decisions that would have led to better outcomes. Finally, we will perform large-scale human subject studies with both laypersons and experts to evaluate their effectiveness in a wide variety of decision making tasks.

Outstanding undergraduate and Masters students are invited to apply to the 9th annual Cornell, Maryland, Max Planck Pre-doctoral Research School. Applications are requested from students in computer and information science, computer engineering, or a related discipline.  The 9th edition of this annual series of week-long schools will focus on emerging research trends in computer science.

The small, select group of attendees will be exposed to state-of-the-art research in computer science, have the opportunity to interact one-on-one with internationally leading scientists from three of the foremost academic institutions in research and higher learning in the US and in Europe, and network with like-minded students. They will get a sense of what it is like to pursue an academic or an industrial research career in computer science and have a head start when applying for graduate school.

For full consideration, applications should be received by February 15, 2025 AOE. Travel and accommodation will be covered for accepted students.

Further information about the school and how to apply can be found at https://cmmrs.mpi-sws.org

MPIs and their partner universities offer a vibrant, dynamic, multi-cultural environment for research and education.  We currently have openings for doctoral positions in several graduate programs. To help you choose which program is the best fit, we recommend you read the short descriptions on the MPI-SWS careers page. You can apply to more than one program, but please do so only if more than one program matches your interests. If you are interested in applying to one or more of these programs, please note that the application deadlines are rapidly approaching.
Highly qualified, broadly interested students who would like to have the opportunity to work with faculty at any MPI or partner university should apply to the cs@max planck program. Applications are due by December 31.
Students who would additionally like to have the opportunity to conduct part of the doctoral program at a top US university should also apply to the Maryland Max Planck Ph.D. Program. Applications are due by December 20.

Students who are already committed to a specific research area should also apply to one of the more specialized programs.

For more information, see the overview of our graduate programs, research careers at MPI-SWS, or apply for positions through our application portal.

MPI-SWS doctoral student Eleni Straitouri was awarded a 2024 Google PhD Fellowship (in Machine Intelligence) to fund her doctoral research on using machine learning to build automated decision support systems that can reliably improve the decisions of human experts.

The Google PhD Fellowship Program was created to recognize outstanding graduate students doing exceptional and innovative research in areas relevant to computer science and related fields. Eleni, who is advised by Manuel Gomez Rodriguez, was one of only 85 recipients worldwide in 2024.

Link: https://research.google/outreach/phd-fellowship/

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

 

Dr. Michael Sammler, who defended his doctoral thesis at Saarland University & MPI-SWS last December, has just received the Runner-Up Prize for the 2024 Informatics Europe Best Dissertation Award!  This is a relatively new international dissertation award in computer science (initiated in 2023).  There were 23 nominations from across Europe this year (maximum 1 per university), and Michael's was ranked one of the top 3 dissertations.

Michael's dissertation is entitled "Automated and Foundational Verification of Low-Level Programs", and was supervised by MPI-SWS faculty Deepak Garg and Derek Dreyer.

Michael's dissertation has also received the Dr. Eduard Martin Prize from Saarland University.

Michael is currently doing a postdoc at ETH Zurich with Peter Müller, and in January 2025 he will start as a tenure-track faculty at IST Austria.

Congratulations, Michael, on this richly deserved honor!!!

The Max Planck Institutes (MPIs) for Informatics, for Security & Privacy, and for Software Systems invite applications for tenure-track faculty in all areas of computer science and its intersection with other disciplines. We expect to fill several positions.

A doctoral degree in computer science or related fields and an outstanding research record are required. Successful candidates are expected to build a team and pursue a highly visible research agenda, both independently and in collaboration with other groups.

The institutes are part of a network of over 80 MPIs, Germany’s premier basic-research institutes. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institutes offer a unique environment that combines the best aspects of a university department and a research laboratory: Faculty enjoy full academic freedom, lead a team of doctoral students and post-docs, and have the opportunity to teach university courses; at the same time, they enjoy ongoing institutional funding in addition to third-party funds, a technical infrastructure unrivaled for an academic institution, as well as internationally competitive compensation.

We maintain an international and diverse work environment and seek applications from outstanding researchers worldwide. The working language is English; knowledge of the German language is not required for a successful career at the institutes.

Qualified candidates should apply using the application portal at https://shlink.mpi-sws.org/faculty. For full consideration, applications should be submitted by December 1st, 2024.

MPIs are committed to fostering a diverse, inclusive, and global academic community, and consider qualified applicants for employment without discrimination on the basis of gender, race, disability, ethnic or social origin, or any other legally protected status. We particularly encourage applications from groups that are underrepresented in computer science. We welcome applications from dual-career couples and will do our best to try and accommodate their needs.

The initial tenure-track appointment is for six years. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

* W2 German Federal Civil Service Renumeration Act (BBesG)

Andrea Lattuada will join MPI-SWS as a Research Group Leader in September 2024. Before joining MPI-SWS, Andrea worked as a researcher in the VMware Research Group. He completed his PhD at ETH Zurich, where he focused on systems for distributed data processing and systems software verification.

Andrea builds verification tools and formally verified systems with a focus on pragmatism. He co-started and co-leads the Verus project. Verus is a tool used by various industry and academic projects to rapidly verify the correctness of systems code written in Rust. At MPI, his research group will continue to leverage software verification to substantially improve the safety and reliability of systems software. This will involve developing new and more powerful techniques to reason about complex software, improving the usability and efficiency of verification tools, and devising principled and cost-effective development disciplines for verified software. Andrea also collaborates with researchers at ETH Zürich on new programming models for the cloud, and on building a verified operating system with a compact, well-specified programming interface.

Andrea’s group has open positions for doctoral students, postdocs, and interns who are interested in working on systems software verification. Current projects focus on making verification more practical and usable by engineers and on leveraging advanced reasoning techniques to tackle complex software. Andrea’s website has more details on his research profile.

The paper "On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates", by Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala and James Worrell, was selected as one of 7 "Distinguished Papers" at LICS 2024.

Distinguished Paper awards are given to about 10% of papers at LICS. These are papers that, in the view of the LICS program committee, make exceptionally strong contribution to the field and should be read by a broad audience due their relevance, originality, significance and clarity.

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 7 papers accepted to POPL 2024.  This is the seventh year in a row that MPI-SWS researchers have published 5+ papers in POPL.  Congratulations to all our POPL authors!

• Decision and Complexity of Dolev-Yao Hyperproperties by Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind


• Parikh's Theorem Made Symbolic by Matthew Hague, Artur Jez, Anthony Widjaja Lin


• Positive Almost-Sure Termination – Complexity and Proof Rules by Rupak Majumdar and V.R. Sathiyanarayana.


• Ramsey Quantifiers in Linear Arithmetics by Pascal Bergsträßer, Moses Ganardi, Anthony Widjaja Lin, Georg Zetzsche


• Reachability in Continuous Pushdown VASS by A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche


• Regular Abstractions for Array Systems by Chih-Duo Hong and Anthony Widjaja Lin


• Securing Verified IO Programs Against Unverified Code in F* by Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter