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

MPI-SWS PhD students Michalis Kokologiannakis and Michael Sammler have accepted tenure-track faculty positions at ETH Zurich and the Institute of Science and Technology Austria, respectively.

Michalis Kokologiannakis, a doctoral student in the Software Analysis and Verification group, has accepted a tenure-track faculty position at ETH Zurich. Michalis is broadly interested in programming languages, compilers, weak memory models, and software verification. More specifically, he is interested in developing novel algorithmic techniques for verifying concurrent software, while also taking into account the weak memory models employed by modern microprocessors. You can find out more about his work at https://people.mpi-sws.org/~michalis/.

Michael Sammler, a doctoral student in the Foundations of Computer Security and Foundations of Programming groups, has accepted a tenure-track faculty position at the Institute of Science and Technology Austria (ISTA). Before starting at ISTA, he will spend one year as a postdoctoral fellow in the Programming Methodology Group at ETH Zurich. Michael's research interests lie in implementing efficient and practical systems and formally proving properties about them. In particular, his research focuses on building formal verification tools for low-level systems code that combine foundational proofs in a proof assistant with a high degree of automation. You can find out more about his work at https://people.mpi-sws.org/~msammler/ and https://ista.ac.at/en/research/sammler-group/.

Congratulations Michael and Michalis!

Anne-Kathrin Schmuck has been appointed as new tenure-track faculty as of July 1st, 2023, after leading a prestigious externally funded Emmy-Noether research group hosted at MPI-SWS since 2020. Her group conducts fundamental research at the intersection of control engineering, cybernetics, and computer science to develop reliable and performant control software for cyber-physical systems. In particular, her work addresses the challenge of orchestrating continuous physical components and discrete logical decision making units within these highly automated and safety-critical technological systems.

Anne has been part of the MPI-SWS faculty as an independent research group leader since 2020. She holds a Dipl.-Ing. (M.Sc.) degree in engineering cybernetics from OvGU Magdeburg, Germany and a Dr.-Ing. (Ph.D.) degree in electrical engineering from TU Berlin, Germany. She joined MPI-SWS as a postdoctoral researcher in the area of formal methods in 2015.

Pramod Bhatotia, who completed his doctoral studies at MPI-SWS, has received the 2023 EuroSys Jochen Liedtke Young Researcher Award.

The EuroSys Jochen Liedtke Young Researcher Award was created in 2014 by ACM EuroSys to reward junior European researchers who have demonstrated exceptional creativity and innovation in systems research, broadly construed. The award is given annually at the EuroSys conference, in memory of Jochen and his fundamental contributions to the systems community. The award is accompanied by a 2,000 EUR cash prize generously provided by RedHat.

Congratulations, Pramod!

MPI-SWS faculty member Derek Dreyer and nine of his collaborators (including notably UdS/MPI alumnus Ralf Jung, as well as former MPI-SWS postdocs Jacques-Henri Jourdan and Aaron Turon and UdS/MPI student David Swasey) have received the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation for their seminal work on the Iris framework for higher-order concurrent separation logic, specifically the following four papers:

• Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer: “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning”. POPL 2015.
• Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ICFP 2016.
• Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. ESOP 2017.
• Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).

The Church Award has been given out since 2016, and has typically been given to papers that were 20-25 years old (to allow time for foundational work on logic to have major impact).  In this case, however, the four awarded Iris papers were published only 5-8 years ago! In that relatively short period of time, Iris has served as a springboard for a huge amount of research in semantics and program verification, including over 70 papers in top venues (see the Iris project page), and it has been adopted as a core verification technology by a multitude of research groups around the world, as well as the systems verification company BedRock Systems.

More details about the Alonzo Church Award and about the 2023 Church Award.

Kaushik Mallik's thesis, entitled Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems, has been recognized with the 2023 ETAPS Doctoral Dissertation Award. The award is given to the PhD student who has made the most original and influential contribution to the research areas in the scope of the ETAPS conferences, and has graduated at a European academic institution. Kaushik was advised by MPI-SWS faculty member Rupak Majumdar.

This is the second time that the ETAPS Doctoral Dissertation Award was given to an MPI-SWS student. In 2021 it was awarded to Ralf Jung for his thesis on Understanding and Evolving the Rust Programming Language, supervised by Derek Dreyer.

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.

The Max Planck Institutes in Computer Science invite applications for tenure-track faculty in all areas of computer science. We expect to fill several positions.

A doctoral degree in computer science or related areas 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 Max Planck Institutes, Germany's premier basic-research organisations. 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 postdocs, 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 on our application website (apply.cis.mpg.de). Review of applications will begin by December 1st, 2022.

The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended to seven years based on a positive midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

Ralf Jung, a doctoral student in the Foundations of Programming group, has accepted a position as a tenure-track assistant professor in the Department of Computer Science at ETH Zurich, Switzerland. Congratulations Ralf!

Ralf's primary research interest is in developing formal foundations and tools that establish machine-checked guarantees for real-world software systems. To achieve this, his work spans all the way from foundational and deeply theoretical to applied, from proving theorems to developing tools used by other researchers and software developers.. You can find out more about his work at https://research.ralfj.de/.

MPI-SWS doctoral student Simon Spies was awarded a 2022 Google PhD Fellowship to fund his doctoral research on Quiver, a verification tool for inferring functional correctness specifications in separation logic.

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. Simon, who is advised by Derek Dreyer, was the only student in the area of Programming Technology and Software Engineering to receive a fellowship in 2022.

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

Mariya Toneva joins the tenure-track faculty at our institute starting September 2022. Mariya’s research is at the intersection of machine learning, natural language processing, and neuroscience. Her group bridges language in machines with language in the brain, with a focus on building computational models of language processing in the brain that can also improve natural language processing systems.

Prior to joining MPI-SWS, Mariya conducted research as a C.V. Starr Fellow at the Princeton Neuroscience Institute. She received her Ph.D. in a joint program between Machine Learning and Neural Computation from Carnegie Mellon University, and her B.S. in Computer Science and Cognitive Science from Yale University.

MPI-SWS Director Derek Dreyer has been selected as the program chair of the 51st ACM SIGPLAN Symposium on Principles of Programming (POPL'24), to be held in London January 17–19, 2024.

POPL is the premier venue in the area of programming languages and, alongside PLDI, ranks as one of the top two international conferences on this topic.

Principles of Programming Languages is the premier forum for the fundamental innovations in design, definition, analysis, transformation, and implementation of programming languages, programming systems, and programming abstractions.

MPI-SWS faculty member Rupak Majumdar has received the 2022 CONCUR Test-of-Time Award for his CONCUR 2003 paper on The Element of Surprise in Timed Games. The work was done in collaboration with Luca de Alfaro, Marco Faella, Thomas A. Henzinger, and Mariëlle Stoelinga.

The award citation reads as follows: "The paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. A key contribution of the paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise as they are played "faster", and the definition of natural concepts of winning conditions for the two players -- ensuring that players can win only by playing according to a physically meaningful strategy. This approach provides a clean answer to the problem of time convergence, and the responsibility of the players in it. For this reason, it has since been the basis of numerous works on timed games. The algorithm established in the paper to study omega-regular conditions in this neat model of timed games is also enticing, resorting to mu-calculus on a cleverly enriched structure."

MPI-SWS faculty member Viktor Vafeiadis has received the 2022 Robin Milner Young Researcher Award, which is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages.  The award citation reads as follows:

"Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep, the first extension of concurrent separation logic to support formal proofs about fine-grained concurrent algorithms.  His work on Cave presented the first fully automatic verifier for establishing linearizability of a class of concurrent data structures, including ones with non-fixed linearization points. His work on CompCertTSO presented the first verified compiler for a concurrent language under a relaxed memory model. He developed the first direct (and mechanized) proof of soundness for concurrent separation logic (CSL) based on operational semantics—beautifully simple compared to prior proofs and a key enabler for proving soundness of more advanced program logics like CAP and Iris. He developed the first separation logic for the C/C++ relaxed memory model—a tour-de-force achievement compared to the standard CSL which assumes sequential consistency. This spawned a whole body of work on modular verification of concurrent data structures under relaxed memory models. His work has found and corrected a number of serious flaws in the C/C++ concurrency model, which led to changes in the C++ standard. And his "promising" semantics for relaxed-memory concurrency offered one of the first viable solutions to the 30-year-old "out-of-thin-air" problem and spawned much follow-on work. His work on GenMC presented the first efficient model checkers for relaxed-memory C/C++ programs with optimality guarantees about their state space exploration. Recent work together with his postdoc Azalea Raad (now faculty at Imperial), presented the first "persistency semantics" for non-volatile memory on multicore architectures. Viktor is not only highly-cited and incredibly prolific—he is also a true pioneer, repeatedly exploring dauntingly technical problems in the semantics and verification of concurrent programs before others dare to try."

This award makes MPI-SWS the only institution in the world to boast two recipients of the SIGPLAN Milner award among its faculty.

Two MPI-SWS faculty, Maria Christakis and Elissa Redmiles, have earned highly competitive Google Research Scholar awards. Maria Christakis's award was given for her research on metamorphic specification and testing of machine-learning models and Elissa Redmiles's award was given for her research on aligning technical data privacy protections with user concerns.

The Google Research Scholar Program provides unrestricted gifts of up to $60,000 to support research at institutions around the world and is focused on funding world-class research conducted by early-career professors. Award proposals go through an internal, merit-based review process and selected faculty can receive a Google Research Scholar award only once in their career. Award recipients are assigned a liaison at the company to share findings with and as a point of contact for further collaboration.

Derek Dreyer, head of the Foundations of Programming research group since 2008, has been appointed as a Scientific Member of the Max Planck Society and Scientific Director of MPI-SWS as of May 1, 2022.

Derek became known for his pioneering work in programming languages and verification, with a particular emphasis on building rigorous foundations for establishing the reliability and correctness of realistic software systems.  In recent years, he and his group have become especially well known for their work on the Iris and RustBelt verification frameworks, both implemented in the Coq proof assistant.  Developed initially in 2015, Iris is a system for developing and deploying higher-order concurrent separation logics; though only 7 years old, it has already been used in over 60 papers published in top venues in programming languages.  One of the most significant applications of Iris is RustBelt, which constitutes the first formal, machine-checked foundation for verifying the safety of the increasingly popular systems programming language Rust.  These large-scale verification efforts place Dreyer's group at the forefront of programming languages research worldwide.

Derek has received numerous accolades for his research, teaching, and service, including the 2017 ACM SIGPLAN Robin Milner Young Researcher Award, a 2015 ERC Consolidator Grant, multiple Distinguished Paper Awards at top conferences like POPL, PLDI, and OOPSLA, the OOPSLA'18 Distinguished Reviewer Award, and most recently, the "Busy Beaver Award" at Saarland University for outstanding commitment to teaching. Under his mentorship, members of his group have also received numerous awards, including the prestigious ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award and ACM Doctoral Dissertation Honorable Mention Award (for Dr. Ralf Jung).

Derek was born in New York City in 1980.  He holds a Bachelor's in Mathematics and Computer Science from New York University and received his PhD in Computer Science from Carnegie Mellon University in 2005. From 2005 to 2007, he was a Research Assistant Professor at the Toyota Technological Institute at Chicago.  He joined MPI-SWS as a tenure-track faculty in January 2008, only a few years after the Institute's founding, and has been an integral member ever since. We are thus very proud to be able to retain him as a Scientific Director of the institute.

Sandra Kiefer has joined MPI-SWS as a research group leader, effective April 1, 2022. Her research interests include algorithmic and structural graph theory as well as logic in computer science, with a recent focus on the applicability of tools from these areas to the study of biochemical networks.

Sandra obtained her Ph.D. from RWTH Aachen University. For her work on combinatorial and logical approaches to graph comparison, she received the Ackermann Award 2020, the EACSL Outstanding Dissertation Award for Logic in Computer Science. After her Ph.D. studies, Sandra was a postdoctoral researcher at RWTH and at the University of Warsaw. She holds Bachelor’s degrees in Bioinformatics and Mathematics and a Master’s degree in Mathematics from Goethe University Frankfurt. She has also completed an M.Ed. degree in Mathematics and Spanish.

MPI-SWS researchers Jiarui Gan, Rupak Majumdar, Goran Radanovic, and Adish Singla have received an Outstanding Paper Award Honorable Mention at AAAI 2022, for their paper "Bayesian Persuasion in Sequential Decision-Making."

The AAAI conference is one of the leading international venues for AI research, covering all sub-areas of the field. AAAI 2022 received more than 9000 submissions, of which 1370 were accepted for publication. Of these 1370 papers, only three papers were selected for an outstanding paper award. Of these three outstanding papers, two were authored by researchers at the Saarland Informatics Campus.

MPI-SWS scientific director Joël Ouaknine was appointed as a Fellow by the Association for Computing Machinery (ACM), the largest computer science association in the world, Joel, who leads the “Foundations of Algorithmic Verification” research group, was appointed ACM fellow for his contributions to algorithmic analysis of dynamical systems.

ACM has also elected as Fellows two researchers from our neighboring Max Planck Institute for Informatics: Thomas Lengauer is recognized for contributions to bioinformatics and medical informatics and Bernt Schiele is recognized for contributions to large-scale object recognition, human detection, and pose estimation.

The ACM Fellows program recognizes the 1% of ACM members who have made the most outstanding achievements in the field of computer and information technology. Worldwide 71 new ACM Fellows were elected this year, twelve of them in Europe, four in Germany and three of them in Saarbrücken.

Further Information: 

• https://www.acm.org/media-center/2022/january/fellows-2021


• https://awards.acm.org/fellows/award-winners


• https://www.mpi-sws.org/people/joel/

Bob Harper, an MPI-SWS external scientific member, has received the 2021 ACM SIGPLAN Programming Languages Achievement Award---the most significant international career award in programming languages. He received the award for his "foundational contributions to our understanding of type theory and its use in the design, specification, implementation, and verification of modern programming languages".

Award Citation:

Robert (Bob) Harper is widely known for his foundational contributions to our understanding of type theory and its use in the design, specification, implementation, and verification of modern programming languages. Bob demonstrated that sound type systems and operational semantics are not only appropriate vehicles for reasoning about idealized languages, but that this theory can be applied to complex, modern languages. His achievements include analysis of language features ranging from references to continuations to modules, the definition of a variety of new type systems, the idea of using types throughout the compilation process, the analysis of run-time system semantics and cost, a formal definition of Standard ML and its mechanization, the definition of logical framework LF and other logical frameworks based on homotopy type theory.

Some of Bob’s most influential work involved the design, theory and implementation of the TIL (Typed Intermediate Language) compiler system, which pioneered the idea that compilers can propagate type information to lower-level intermediate languages, where it can be used to guide optimizations and to catch compiler bugs. These ideas led directly to the development of proof-carrying code, typed assembly language, and a wide array of type-preserving compilers.

Bob Harper has also had a profound impact though his mentorship, teaching and the influence of his books “Programming in Standard ML” and “Practical Foundations for Programming Languages.”

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.

Researchers from MPI-SWS have authored a total of 11 papers accepted to POPL 2022 (just under 17% of all accepted papers).  This is the fifth year in a row that MPI-SWS researchers have published 5+ papers in POPL.  Furthermore, two Max Planck papers were awarded a 2022 POPL Distinguished Paper Award. Congratulations to all our POPL authors!

• Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn


• Context-Bounded Verification of Thread Pools  Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche


• Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal Stores Azalea Raad, Luc Maranget, Viktor Vafeiadis


• Isolation Without Taxation: Near Zero Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Ravi Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan


• Pirouette: Higher-Order Typed Functional Choreographies Andrew K. Hirsch, Deepak Garg. DISTINGUISHED PAPER


• Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations  Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer.  DISTINGUISHED PAPER


• Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Ruemmer, Zhilin Wu


• Subcubic Certificates for CFL Reachability Dmitry Chistikov, Rupak Majumdar, Philipp Schepper


• Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis


• VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell


• What's Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell

The Max Planck Institutes for Informatics (Saarbruecken), Software Systems (Saarbruecken and Kaiserslautern), and Security and Privacy (Bochum) invite applications for tenure-track faculty in all areas of computer science. We expect to fill several positions.

A doctoral degree in computer science or related areas 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 Max Planck Institutes, Germany's premier basic-research organisations. 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 postdocs, 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 on our application website (apply.cis.mpg.de). Review of applications will begin by December 1st, 2021.

The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended to seven years based on a positive midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

Antoine Kaufmann has joined the tenure-track faculty at our institute, effective October 1, 2021.  He has been a member of our faculty as a research group leader since joining MPI-SWS in August 2018.  Antoine's research centers on the interplay of software and hardware in modern systems.  He is interested in the nascent challenges in designing, implementing, and maintaining hardware-software systems for different application domains, starting with data center networking and machine learning.

Prior to joining MPI-SWS, Antoine received his Ph.D. from the University of Washington, and his Master's and Bachelor's degrees from ETH Zurich.

Ralf Jung's thesis, entitled Understanding and Evolving the Rust Programming Language, has been recognized with the 2021 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award. (The award this year was shared with Gagandeep Singh, a doctoral student at ETH Zurich). Ralf was advised by MPI-SWS faculty member Derek Dreyer.

This is the second year in a row that the ACM SIGPLAN Dissertation Award was given to an MPI-SWS student. Last year it was awarded to Filip Niksic for his thesis on Combinatorial Constructions for Effective Testing, supervised by Rupak Majumdar.

The award, first given in 2001, recognizes outstanding doctoral dissertations in the area of Programming Languages.

Ralf Jung's doctoral dissertation on "Understanding and Evolving the Rust Programming Language" has received the ACM Doctoral Dissertation Award Honorable Mention. The ACM Doctoral Dissertation Award is considered to be one of the most prestigious international dissertation awards in the area of computer science, and there are only two Honorable Mentions given for the award each year. The Honorable Mention Award comes with a prize of $10,000 and an invitation to accept the award at the annual ACM Awards Banquet in San Francisco.

Ralf's work has previously received the ETAPS Doctoral Dissertation Award and the Otto Hahn Medal, as well as being featured in the April 2021 issue of Communications of the ACM in an article entitled "Safe Systems Programming in Rust". For more details see the Saarland Informatics Campus press release.

Ralf Jung and Bilal Zafar have each been awarded a 2021 Otto Hahn Medal for outstanding scientific achievement. The Max Planck Society awards the Otto Hahn Medal annually to young scientists in recognition of outstanding scientific achievement. Ralf was awarded the medal for his work on the first formal foundations for the cutting-edge systems programming language Rust, while Bilal was awarded the medal for his work on developing responsible and trustworthy AI systems that can help reduce discrimination and polarisation in society. Ralf obtained his PhD in August 2020, and was advised by Derek Dreyer. Ralf is now a postdoc at MPI-SWS and research affiliate at MIT. Bilal obtained his PhD in February 2019, and was advised by Krishna Gummadi and Manuel Gomez Rodriguez. Bilal is now an Applied Scientist at Amazon Web Services.

Ralf Jung's doctoral dissertation on "Understanding and Evolving the Rust Programming Language" has received the ETAPS Doctoral Dissertation Award for 2021. The award is given to the PhD student who has made the most original and influential contribution to the research areas in the scope of the ETAPS conferences, and has graduated in 2021 at a European academic institution. Ralf was advised by MPI-SWS faculty member Derek Dreyer.

A committee of international experts evaluated candidate dissertations with respect to originality, relevance, and impact to the field, as well as the quality of writing. The committee found that Dr. Ralf Jung's dissertation is very well-written and makes several highly original contributions in the area of programming language semantics and verification. The committee was also particularly impressed by the dissertation for its technical depth, the quality and quantity of the associated published work, as well as its relevance and impact both in academia and industry.

Ralf's work on Rust was also featured in a recent Communications of the ACM article: Safe Systems Programming in Rust by Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. The article appeared in the April 2021 issue of CACM, together with a short video about this work produced by ACM.

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the new Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 8 papers accepted to POPL 2021 (over 10% of all accepted papers).  This is the fourth year in a row that MPI-SWS researchers have published 5+ papers in POPL.  Furthermore, two Max Planck papers were awarded a Distinguished Paper Award. Congratulations to all our POPL authors!

MPI-SWS papers:

• A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann


• Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche DISTINGUISHED PAPER


• Deciding ω-Regular Properties on Linear Recurrence Sequences Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell


• Giving Semantics to Program-Counter Labels via Secure Effects Andrew Hirsch, Ethan Cecchetti


• PerSeVerE: Persistency Semantics for Verification under Ext4 Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis


• Transfinite Step-Indexing for Termination Simon Spies, Neel Krishnaswami, Derek Dreyer

MPI-SP papers:

• A Pre-Expectation Calculus for Probabilistic Sensitivity Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja DISTINGUISHED PAPER


• Deciding Accuracy of Differential Privacy Schemes Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan

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).

Filip Niksic's thesis on "Combinatorial Constructions for Effective Testing" has won the John C. Reynolds Doctoral Dissertation Award for 2020. This is an annual award given by ACM SIGPLAN for a doctoral dissertation in the field of programming languages. Filip was advised by MPI-SWS faculty member Rupak Majumdar.

The award citation reads as follows: Soundness is at the core of most programming language verification techniques. On the other hand, random testing is one of the most commonly used techniques for analyzing software. Developing a theory of soundness for random testing is therefore a very important goal, but very few results existed before this thesis.Randomized techniques are seldom used in (sound) program analyses, which means that addressing the problem required the development of new ways to approaching it. Filip Niksic's thesis is among the first to apply deep techniques from randomized algorithms and combinatorics to the problem of understanding and explaining the effectiveness of random testing. Moreover, the theory helps with the design of new random testing approaches. The thesis addresses a hard problem, brining in novel theory from outside programming languages, and proving hard theorems. As scientists, when we see a phenomenon that we cannot immediately explain (in this case, the effectiveness of random testing), we should try to build a scientific explanation. For some problems, including random testing, it is unclear that one can actually formulate a precise theory, because the "real world" is extremely messy. The fact that Filip Niksic is able to formulate such problems precisely and prove nontrivial theorems about them is surprising and opens the door to a new field.

The third Salomaa prize has been awarded to MPI-SWS director Joël Ouaknine and James Worrell (Professor of Computer Science at Oxford University), for their outstanding contribution to Theoretical Computer Science, in particular to the theory of timed automata and to the analysis of dynamical systems.

The Salomaa prize in Automata Theory, Formal Languages and Related Topics is awarded each year by the Developments in Language Theory (DLT) Symposium. It was named to honour the scientific achievements and influence of Arto Salomaa, a founder of the DLT symposium. The prize consists of 2000 euros, funded by the University of Turku, Finland, the home university of Arto Salomaa.

 

The Max Planck Institutes for Informatics (Saarbruecken), Software Systems (Saarbruecken and Kaiserslautern), and Security and Privacy (Bochum), invite applications for tenure-track faculty in all areas of computer science. We expect to fill several positions.

A doctoral degree in computer science or related areas 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 Max Planck Institutes, Germany's premier basic-research organisations. 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 postdocs, 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 on our application website (apply.cis.mpg.de). To receive full consideration, applications should be received by December 15th, 2020.

The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended to seven years based on a positive midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

Ever since the birth of Artificial Intelligence (AI) at the Dartmouth workshop in 1956, researchers have debated about the exact role that AI will play, and should play, in society. While some have envisioned a romanticized version of AI, incorporated into the narratives of 20th century movies, successful AI developments are often closer to J. C. R. Licklider’s vision of AI, which puts an emphasis on a collaborative relationship between humans and AI, and focuses on hybrid human-AI decision making.

In the Multi-Agent Systems group at MPI-SWS, we study multi-agent sequential decision making using formal frameworks that can capture nuances often presented in human-AI collaborative settings. Specifically, we study different aspects of agent-to-agent interaction in settings where agents share a common goal, but can have different perceptions of reality. The overall goal is to design a more effective AI decision maker that accounts for the behavior of its collaborators, and compensates for their imperfections. To achieve this goal, the AI decision maker can use steering policies to nudge its collaborators to adopt better policies, i.e., policies that lead to an improved joint outcome. In what follows, we summarize some of our recent results related to this agenda.

Accounting for misaligned world-views. An effective way to model behavioral differences between humans and modern AI tools (based on machine learning) is through a model that captures the misalignment in how the agents perceive their environment. Using this approach, we have proposed a new computational model, called Multi-View Decision Process, suitable for modeling two-agent cooperative scenarios in which agents agree on their goals, but disagree on how their actions affect the state of the world [1]. This framework enables us to formally analyze the utility of accounting for the misalignment in agents’ world-views when only one of the agents has a correct model of the world. Our results show that modeling such a misalignment is not only beneficial, but critical. The main takeaway is that to facilitate a more successful collaboration among agents, it is not sufficient to make one agent (more) accurate in its world-view: naively improving the accuracy of one agent can degrade the joint performance unless one explicitly accounts for the imperfections of the other agent. To this end, we have developed an algorithm for finding an approximately optimal steering policy for the agent with the correct world-view.

Adapting to a non-stationary collaborator. In addition to accounting for a misalignment in world-views, decision makers must also account for the effects of their behavior on other agents. Namely, decision makers respond to each other's behavior, leading to behavior which is non-stationary and changes over time. In the context of human-AI collaboration, this might happen if the human agent changes their behavior over time, for example, as it learns to interact with the AI agent. Such non-stationary behavior of the human agent could have a negative impact on the collaboration, and can lead to a substantially worse performance unless the AI agent adapts to the changing behavior of the human agent. We can model this situation with a two-agent setting similar to the one presented above, but which allows agents to change their behavior as they interact over time [2]. The agent with the correct world-view now has to adapt to the non-stationary behavior of its collaborator. We have proposed a learning procedure that has provable guarantees on the joint performance under the assumption that the behavior of the other agent is not abruptly changing over time. We have shown that this assumption is not trivial to relax in that obtaining the same guarantees without this assumption would require solving a computationally intractable problem.

Steering via environment design. The previous two cases consider indirect steering policies for which the agent with the correct model implicitly influences the behavior of its collaborator by acting in the world. A more explicit influence would be obtained if the actions of this agent are directly changing the world-view of its collaborator. In the context of human-AI collaboration, the AI agent could shape the environment to nudge the human agent to adopt a more efficient decision policy. This can be done through reward shaping, i.e., by making some actions more costly for humans in terms of effort, or through dynamics shaping, i.e., by changing the perceived influence that the human’s actions have on the world. In the machine learning terminology, such a steering strategy is nothing else but a form of an adversarial attack of the AI agent (attacker) on the human agent. In our recent work [3], we have characterized how to optimally perform these types of attacks and how costly they are from an attacker’s point of view.

 

References: 

[1] Dimitrakakis, C., Parkes, D.C., Radanovic, G. and Tylkin, P., 2017. Multi-view Decision Processes: The Helper-AI Problem. In Advances in Neural Information Processing Systems.

[2] Radanovic, G., Devidze, R., Parkes, D. and Singla, A., 2019. Learning to Collaborate in Markov Decision Processes. In International Conference on Machine Learning.

[3] Rakhsha, A., Radanovic, G., Devidze, R., Zhu, X. and Singla, A., 2020. Policy Teaching via Environment Poisoning: Training-time Adversarial Attacks against Reinforcement Learning. In International Conference on Machine Learning.

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.

Anne-Kathrin Schmuck, a postdoctoral fellow in the Rigorous Software Engineering group, was accepted to the Emmy Noether Programme of the German Science Foundation (DFG). This grant programme is the most prestigious programme for early career researchers from the DFG. It provides funding for an independent research group for a period of six years.

Anne-Kathrin's group will be hosted at MPI-SWS in Kaiserslautern and will develop automated modular synthesis techniques for reliable Cyber-Physical System (CPS) design. Her work draws inspiration from both Control Theory and Computer Science and centers around Reactive Synthesis, Supervisory Control Theory and Abstraction-Based Controller Design.

Aastha Mehta, a doctoral student in the Distributed Systems group and the Security & Privacy group, has accepted a position as a tenure-track assistant professor in the Department of Computer Science at University of British Columbia, Vancouver, Canada. Congratulations Aastha!

Aastha's research interests span systems security, data privacy, operating systems, and distributed systems. She has worked on building systems for ensuring policy compliance and for mitigating network side-channel leaks in online services. You can find out more about her work at https://people.mpi-sws.org/~aasthakm/.

Researchers from the Max Planck Institute for Software Systems (MPI-SWS), the Max Planck Institute for Informatics (MPI-INF), and the Max Planck Institute for Security and Privacy (MPI-SP) have coauthored 17 papers at the colocated LICS 2020 and ICALP 2020, two of the top conferences in theoretical computer science. LICS is the premier conference on logic in computer science and ICALP is the flagship conference of the European Association for Theoretical Computer Science.

MPI-SWS papers:

1. Invariants for Continuous Linear Dynamical Systems. Shaull Almagor, Edon Kelmendi, Joël Ouaknine and James Worrell. ICALP 2020, Track B. [ Video | Paper]


2. The complexity of bounded context switching with dynamic thread creation. Pascal Baumann, Rupak Majumdar, Ramanathan Thinniyam Srinivasan and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]


3. Extensions of ω-Regular Languages. Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański and Georg Zetzsche. LICS 2020. [ Video | Paper ]


4. Rational subsets of Baumslag-Solitar groups. Michaël Cadilhac, Dmitry Chistikov and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]


5. On polynomial recursive sequences. Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk and Géraud Sénizergues. ICALP 2020, Track B. [ Video | Paper ]


6. An Approach to Regular Separability in Vector Addition Systems. Wojciech Czerwiński and Georg Zetzsche. LICS 2020. [ Video | Paper ]


7. The complexity of knapsack problems in wreath products. Michael Figelius, Moses Ganardi, Markus Lohrey and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]


8. The Complexity of Verifying Loop-free Programs as Differentially Private. Marco Gaboardi, Kobbi Nissim and David Purser. ICALP 2020, Track B. [ Video | Paper ]


9. On Decidability of Time-bounded Reachability in CTMDPs. Rupak Majumdar, Mahmoud Salamati and Sadegh Soudjani. ICALP 2020, Track B. [ Video | Paper ]

MPI-INF papers:

1. Scheduling Lower Bounds via AND Subset Sum. Amir Abboud, Karl Bringmann, Danny Hermelin and Dvir Shabtay. ICALP 2020, Track A.  [ Video | Paper ]


2. Faster Minimization of Tardy Processing Time on a Single Machine. Karl Bringmann, Nick Fischer, Danny Hermelin, Dvir Shabtay and Philip Wellnitz. ICALP 2020, Track A. [ Video | Paper ]


3. Hitting Long Directed Cycles is Fixed-Parameter Tractable. Alexander Göke, Dániel Marx and Matthias Mnich. ICALP 2020, Track A. [ Video | Paper ]


4. A (2 + ε)-Factor Approximation Algorithm for Split Vertex Deletion. Daniel Lokshtanov, Pranabendu Misra, Fahad Panolan, Geevarghese Philip and Saket Saurabh. ICALP 2020, Track A. [ Video | Paper ]


5. Hypergraph Isomorphism for Groups with Restricted Composition Factors. Daniel Neuen. ICALP 2020, Track A. [ Video | Paper ]


6. Deterministic Sparse Fourier Transform with an l∞ Guarante. Yi Li and Vasileios Nakos. ICALP 2020, Track A. [ Video | Paper ]

MPI-SP papers:

1. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla and Mahesh Viswanathan. LICS 2020. [ Video | Paper ]


2. Universal equivalence and majority on probabilistic programs over finite fields. Charlie Jacomme, Steve Kremer and Gilles Barthe. LICS 2020. [ Video | Paper ]

Due to the impressive advances in Machine Learning and the unlimited availability of data, neural networks are rapidly becoming prevalent in our everyday lives, for instance by assisting in image-classification or decision-making tasks. As a result, there is growing concern regarding the reliability of neural networks in performing these tasks. In particular, it could be disastrous if an autonomous vehicle misclassifies a street sign, or if a recidivism-risk algorithm, which predicts whether a criminal is likely to re-offend, is unfair with respect to race.

In the Practical Formal Methods group at MPI-SWS, we have recently focused on applying techniques from Software Engineering, including static analysis and test generation, to validate and verify properties of neural networks, such as robustness and fairness. In the following, we give a brief overview of three research directions we have been pursuing in this setting.

Blackbox Fuzzing of Neural Networks

By now, it is well known that even very subtle perturbations of a correctly classified image, such as a street sign, could cause a neural network to classify the new image differently. Such perturbed images are referred to as adversarial inputs and pose a critical threat to important applications of Machine Learning, like autonomous driving.

In our group, we recently developed DeepSearch [1], a blackbox-fuzzing technique that generates adversarial inputs for image-classification neural networks. Starting from a correctly classified image, DeepSearch strategically mutates its pixels such that the resulting image is more likely to be adversarial. By using spatial regularities of images, DeepSearch is able to generate adversarial inputs, while only querying the neural network very few times, which entails increased performance of our technique. Moreover, through a refinement step, DeepSearch further reduces the already subtle pixel perturbations of an adversarial input.

Adversarial-Input Detection for Neural Networks

To protect neural networks against adversarial inputs, we have developed RAID [2], a runtime-monitoring technique for detecting whether an input to a neural network is adversarial. Our technique consists of training a secondary classifier to identify differences in neuron activation values between correctly classified and adversarial inputs. RAID is effective in detecting adversarial inputs across a wide range of adversaries even when it is completely unaware of the type of adversary. In addition, we show that there is a simple extension to RAID that allows it to detect adversarial inputs even when these are generated by an adversary that has access to our detection mechanism.

Fairness Certification of Neural Networks

Several studies have recently raised concerns about the fairness of neural networks. To list a few examples, commercial recidivism-risk and health-care systems have been found to be racially biased. There is also empirical evidence of gender bias in image searches, for instance when searching for “CEO”. And facial-recognition systems, which are increasingly used in law enforcement, have been found biased with respect to both gender and race. Consequently, it is critical that we design tools and techniques for certifying fairness of neural networks or characterizing their bias.

We make an important step toward meeting these needs by designing the LIBRA static-analysis framework [3] for certifying causal fairness of neural networks used for classification of tabular data. In particular, given input features considered sensitive to bias, a neural network is causally fair if its output classification is not affected by different values of the sensitive features. On a high level, our approach combines a forward and a backward static analysis. The forward pass aims to divide the input space into independent partitions such that the backward pass is able to effectively determine fairness of each partition. For the partitions where certification succeeds, LIBRA provides definite (in contrast to probabilistic) fairness guarantees; otherwise, it describes the input space for which bias occurs. We have designed this approach to be sound and configurable with respect to scalability and precision, thus enabling pay-as-you-go fairness certification.

References

[1] Fuyuan Zhang, Sankalan Pal Chowdhury and Maria Christakis. DeepSearch: Simple and Effective Blackbox Fuzzing of Deep Neural Networks. CoRR abs/1910.06296, 2019.

[2] Hasan Ferit Eniser, Maria Christakis and Valentin Wüstholz. RAID: Randomized Adversarial-Input Detection for Neural Networks. CoRR abs/2002.02776, 2020.

[3] Caterina Urban, Maria Christakis, Valentin Wüstholz and Fuyuan Zhang. Perfectly Parallel Fairness Certification of Neural Networks. CoRR abs/1912.02499, 2019.

Software systems have become ubiquitous in our modern world and, consequently, so have bugs and glitches. While many software failures are harmless and often merely annoying, some can have catastrophic consequences. Just imagine the dire results of an autonomous car failing to stop at a red traffic light or a plane's control system becoming unresponsive during takeoff or landing.

In our research, we address these problems and develop intelligent tools that help engineers to build safe and reliable hardware, software, and cyber-physical systems. To this end, we employ a unique and promising strategy, which has recently also regained major attention in the artificial intelligence community: combining inductive techniques from the area of machine learning and deductive techniques from the area of mathematical logic (e.g., see the recent Dagstuhl seminar on "Logic and Learning", which was co-organized by one of our group members). Specifically, our research revolves around three topics, to which the remainder of this article is devoted: verification, synthesis, and formal specification languages.

Verification

Verification is an umbrella term referring to tools and techniques that formally prove that a given system satisfies its specification. In the context of software, a popular approach is deductive verification. The idea is easy to describe: first, the given program is augmented with annotations (typically loop invariants, pre-/post-conditions of method calls, and shape properties of data structures), which capture the developer's intent and facilitate the deductive reasoning in a later step; second, the program, together with its annotations, is translated into formulas in a suitable logic, called verification conditions; third, the verification conditions are checked for validity using automated theorem provers. Thanks to brilliant computer scientists, such as Edsger Dijkstra and Tony Hoare, as well as recent advances in constraint solving, the latter two steps can be (almost) entirely automated. However, the first step still remains a manual, error-prone task that requires significant training, experience, and ingenuity. In fact, this is one of the main obstacles preventing a widespread adaptation of formal verification in practice.

To also automate the challenging first step, we have developed a novel approach, called ICE learning [1], which intertwines inductive and deductive reasoning. The key idea is to pit a (deductive) program verifier against an (inductive) learning algorithm, whose goal is to infer suitable annotations from test-runs of the program and failed verification attempts. The actual learning proceeds in rounds. In each round, the learning algorithm proposes candidate annotations based on the data it has gathered so far. The program verifier then tries to prove the program correct using the proposed annotations. If the verification fails, the verifier reports data back to the learning algorithm explaining why the verification has failed. Based on this new information, the learning algorithm refines its conjecture and proceeds to the next round. The loop stops once the annotations are sufficient to prove the program correct.

ICE learning has proven to be a very powerful approach that allows fully automatic verification of a wide variety of programs, ranging from recursive and concurrent programs over numeric data types [1], to algorithms manipulating dynamically allocated data structures [2], to industry-size GPU kernels [3]. In addition, the principles underlying ICE learning can be lifted to other challenging verification tasks, such as the verification of parameterized systems [4] as well as—in ongoing research—to the verification of cyber-physical and AI-based systems. You might want to try a demo immediately in your browser.

Synthesis

Synthesis goes beyond verification and could be considered the holy grail of computer science. In contrast to checking whether a hand-crafted program meets its specification, the dream is to fully automatically generate software (or a circuit for that matter) from specifications in a correct-by-construction manner.

Although this dream is unrealistic in its whole generality, there exist various application domains in which automated synthesis techniques have been applied with great success. In our own research, for instance, we have developed techniques for synthesizing safety controllers for reactive, cyber-physical systems that have to interact with a complex–and perhaps only partially known–environment [5, 6]. Moreover, we have proposed a general framework for generating loop-free code from input-output examples and specifications written in first-order logic [7]. Similar to ICE learning, these methods combine inductive and deductive reasoning, thereby unveiling and exploiting synergies of modern machine learning algorithms and highly-optimized symbolic reasoning engines.

Formal Specification Languages

Both verification and synthesis rely on the ability to write correct formal specifications, which have to precisely capture the engineer’s intuitive understanding of the system in question. In practice, however, formalizing the requirements of a system is notoriously difficult, and it is well known that the use of standard formalisms such as temporal logics requires a level of sophistication that many users might never develop.

We have recently started a new research project to combat this serious obstacle. Its main objective is to design algorithms that learn formal specifications in interaction with human engineers. As a first step towards this goal, we have developed a learning algorithm for the specification language “Linear Temporal Logic (LTL)”, which is the de facto standard in many verification and synthesis applications. You might think of this algorithm as a recommender system for formal specifications: the human engineer provides examples of the desired and undesired behavior of the system in question, while the recommender generates a series of LTL specifications that are consistent with the given examples; the engineer can then either chose one of the generated specifications or provide additional examples and rerun the recommender.

In ongoing research, we are extending our learning algorithm to a wide range of other specification languages, including Computational Tree Logic, Signal Temporal Logic, and the Property Specification Language. Moreover, we are developing feedback mechanisms that allow for a tighter integration of the human engineer into the loop. Again, you can try our technology immediately in your browser.

References

[1] D’Souza, Deepak; Ezudheen, P.; Garg, Pranav; Madhusudan, P.; Neider, Daniel: Horn-ICE Learning for Synthesizing Invariants and Contracts. In: Proceedings of the ACM on Programming Languages (PACMPL), volume 2 issue OOPSLA, pages 131:1–131:25. ACM, 2018.

[2] Neider, Daniel; Madhusudan, P.; Garg, Pranav; Saha, Shambwaditya; Park, Daejun: Invariant Synthesis for Incomplete Verification Engines. In: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), volume 10805 of Lecture Notes in Computer Science, pages 232–250. Springer, 2018

[3] Neider, Daniel; Saha, Shambwaditya; Garg, Pranav; Madhusudan, P.: Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants. In: 26th International Static Analysis Symposium (SAS 2019), volume 11822 of Lecture Notes in Computer Science, pages 323–346. Springer, 2019

[4] Neider, Daniel; Jansen, Nils: Regular Model Checking Using Solver Technologies and Automata Learning. In: 5th International NASA Formal Method Symposium (NFM 2013), volume 7871 of Lecture Notes in Computer Science, pages 16–31. Springer, 2013

[5] Neider, Daniel; Topcu, Ufuk: An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of Lecture Notes in Computer Science, pages 204–221. Springer, 2016

[6] Neider, Daniel; Markgraf, Oliver: Learning-based Synthesis of Safety Controllers. In: 2019 International Conference on Formal Methods in Computer Aided Design (FMCAD 2019), pages 120–128. IEEE, 2019

[7] Neider, Daniel; Saha, Shambwaditya; Madhusudan, P.: Synthesizing Piece-wise Functions by Learning Classifiers. In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of Lecture Notes in Computer Science, pages 186–203. Springer, 2016

[8] Neider, Daniel; Gavran, Ivan: Learning Linear Temporal Properties. In: 2018 International Conference on Formal Methods in Computer Aided Design (FMCAD 2018), pages 148–157. IEEE, 2018

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the new Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 8 papers accepted to POPL 2020 (over 10% of all accepted papers).  This is the third year in a row that MPI-SWS researchers have published 5 papers in POPL.  Furthermore, MPI-SWS faculty member Derek Dreyer is the first person ever to publish 4 papers in a single POPL.  Congratulations to all our POPL authors!

MPI-SWS papers:

• The Future is Ours: Prophecy Variables in Separation Logic. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs. [pdf]


• The High-Level Benefits of Low-Level Sandboxing. Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak. [pdf]


• Persistency Semantics of the Intel-x86 Architecture. Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis. [pdf]


• RustBelt Meets Relaxed Memory. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. [pdf]


• Stacked Borrows: An Aliasing Model for Rust. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. [pdf]

MPI-SP papers:

• Formal Verification of a Constant-Time Preserving C Compiler. Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu. [pdf]


• A Probabilistic Separation Logic. Gilles Barthe, Justin Hsu, Kevin Liao. [pdf]


• Relational Proofs for Quantum Programs. Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou. [pdf]

The Max Planck Institutes for Informatics (Saarbruecken), Software Systems (Saarbruecken and Kaiserslautern), and Security and Privacy (Bochum), invite applications for tenure-track faculty in all areas of computer science. Pending final approval, we expect to fill several positions.

A doctoral degree in computer science or related areas 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 Max Planck Institutes, Germany's premier basic-research organisations. 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 on our application website (apply.cis.mpg.de). To receive full consideration, applications should be received by December 15th, 2019.

The Max Planck Society wishes to increase the number of women in those areas where they are underrepresented. Women are therefore explicitly encouraged to apply. The Max Planck Society is also committed to increasing the number of employees with severe disabilities in its workforce. Applications from persons with severe disabilities are expressly desired.

The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

Goran Radanovic joined MPI-SWS as a research group leader on Sep 16, 2019. He is generally interested in studying AI systems, and more specifically in the design and analysis of systems with intelligent and self-interested agents. Particular topics of interest include value-aligned artificial intelligence, human-AI collaboration, and decision making systems with societally-aware utility functions. 

Prior to joining MPI-SWS, he was a postdoctoral researcher at Harvard University, where he worked with Prof. David C. Parkes. He received his Ph.D. in Computer Science from the Swiss Federal Institute of Technolgy in Lausanne (EPFL), under the supervision of Prof. Boi Faltings. He obtained his Master’s and Bachelor’s degrees in Computer Science fromthe Faculty of Electrical Engineering and Computing at the University of Zagreb.

Filip Mazowiecki is joining us from the University of Bordeaux, where he spent the last two years as a postdoc. His research area is formal verification, the study of verifying correct functioning of systems. He is mostly interested in the theoretical analysis of models like Petri nets and weighted automata, working on fundamental questions like reachability and equivalence.

Filip obtained his PhD at the University of Warsaw on the topic of database theory. After he obtained his PhD he switched to the area of formal verification, spending almost four years as a postdoc at the Universities of Warwick, Oxford and Bordeaux.

The paper "ERIM: Secure, Efficient, In-process Isolation with Memory Protection Keys (MPK)" received a Distinguished Paper Award at the 2019 Usenix Security Symposium. It was selected as one of 6 distinguished papers out of 113 papers that appeared in the conference proceedings.

The work was also selected as the recipient of the Usenix Internet Defense Prize, along with a USD 100k gift from Facebook to support  further development of the technology.

The paper was authored by MPI-SWS doctoral students Anjo Vahldiek-Oberwagner, Eslam Elnikety, and Michael Sammler, along with MPI-SWS intern Nuno Duarte and MPI-SWS faculty members Deepak Garg and Peter Druschel.

Read more about ERIM here.

Keon Jang has joined the institute as a tenure-track faculty member, effective February 1, 2019. Keon Jang is joining us from Google, where he has been a software engineer since 2016. He is broadly interested in network systems and currently his work focuses on network performance isolation in data-center networks.

Prior to Google, he worked on software support for on network function virtualization (NFV) at Intel Labs. He received his PhD in Computer Science from KAIST, and subsequently held a postdoctoral research position at Microsoft Research Cambridge, UK.

Consider the everyday websites and apps that we use: online shops, news websites, search engines, social networks, navigation apps, instant messaging apps, and many more.  Most of these programs don't just run in isolation on our laptops or phones, but instead connect over the internet to backends and databases running in datacenters across the world.  These backends perform a wide range of tasks, including constructing your personalized social network feed, storing and retrieving comments on message boards, and calculating results for your search query.  From our perspective as users, the actions we perform are simple, such as opening the app and loading our personalized profile.  But under the hood, each action usually results in complex processing across many processes and machines in a datacenter.

It has never been easier to write and deploy complex programs like these.  Cloud computing companies who own datacenters (such as Google, Amazon, and Microsoft) will gladly rent out computer services at a touch of a button, on demand.  Using designs like microservices, it is easy for programmers to construct complex programs out of smaller, simpler building blocks.  There are frameworks and open-source software packages to help developers construct big applications out of small pieces, to spread those pieces out over multiple machines in a datacenter, and to have the pieces communicate and interact with each other over the network.

Problems show up when software goes live.  Compared to developing and deploying the software, it is much harder to make sure everything goes smoothly when the software is up and running.  Distributed computer programs have lots of moving pieces, and there are lots of opportunities for things to go wrong.  For example, if one machine in the datacenter has a hardware problem, or the code is buggy, or too many people are trying to access it at once, the effects can be wide-ranging.  It can create a butterfly effect of problems, which we term cascading failures, that can lead to the app or website as a whole becoming slow, or going down entirely.  It's hard for programmers to get to the bottom of these kinds of problems, because there's no single machine or process doing all the work.  A problem that occurs on one machine might manifest as strange symptoms on a different machine later on.  Figuring out the root cause of a problem is challenging, as is anticipating problems in the first place.  Even big internet companies like Facebook and Google experience problems like this today.

These kinds of problems motivate the research of the Cloud Software Systems Research Group at the Max Planck Institute for Software Systems.  We research ways for operators to understand what's going on in their live distributed system, to troubleshoot problems when they occur at runtime, and to design systems that proactively avoid problems.  One approach we take is to design distributed tracing tools that can be used by the system operators.  The goal of distributed tracing is to record information about what a program does while it's running.  The tools record events, metrics, and performance counters, which together expose the current state and performance of the system, and how it changes over time.  A key additional step taken by distributed tracing tools is to record the causal ordering of events happening in the system — that is, the interactions and dependencies between machines and processes.  Causal ordering is is very useful for diagnosing problems that span multiple processes and machines, especially when there might be lots of concurrent, unrelated activity going on at the same time.  It lets us reconstruct the end-to-end execution paths of requests, across all components and machines, and then reason about the sequence of conditions and events that led up to a problem.  Without causal ordering, this information is missing, and pinpointing the root cause of a problem would be like searching for a needle in a haystack.

The Cloud Software Systems Research Group has looked at a number of challenges in making distributed tracing tools efficient, scalable, and more widely deployable. In our recent work, we have thought about how you can efficiently insert instrumentation to record entirely new information, into an already-running system, without having to rebuild or restart the system [1].  We have looked at problems in dealing with the large volume of data generated by distributed tracing tools, and deciding which data is most valuable to keep if there's not enough room to keep it all [2].  We have also considered the implications of distributed tracing at extremely large scale, and how to efficiently collect, aggregate, and process tracing data in real-time [3].

In our ongoing work, we are investigating ways for the data recorded by tracing tools to feed back in to decisions made by datacenter infrastructure, such as resource management, scheduling, and load balancing.  We are also considering new challenges that arise in scalable data analysis: how do you analyze large datasets of traces and derive insights about aggregate system behavior?  One approach we are exploring uses techniques in representational machine learning, to transform richly annotated tracing data into a more tractable form for interactive analysis.  More broadly, our group investigates a variety of approaches besides just distributed tracing tools, including ways to better design and develop the distributed systems in the first place.  Ultimately, our goal is to make modern cloud systems easier to operate, understand, and diagnose.

References

[1] Jonathan Mace, Ryan Roelke, and Rodrigo Fonseca.  Pivot Tracing: Dynamic Causal Monitoring for Distributed Systems.  In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP '15), 2015.

[2] Pedro Las-Casas, Jonathan Mace, Dorgival Guedes, and Rodrigo Fonseca.  Weighted Sampling of Execution Traces: Capturing More Needles and Less Hay.  In Proceedings of the 9th ACM Symposium on Cloud Computing (SoCC'18), 2018.

[3] Jonathan Kaldor, Jonathan Mace, Michał Bejda, Edison Gao, Wiktor Kuropatwa, Joe O'Neill, Kian Win Ong, Bill Schaller, Pingjia Shan, Brendan Viscomi, Vinod Venkataraman, Kaushik Veeraraghavan, Yee Jiun Song.  Canopy: An End-to-End Performance Tracing And Analysis System. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP '17), 2017.

A long-standing problem both within research and in society generally is that of how to analyze data about people without risking the privacy of those people. There is an ever-growing amount of data about people: medical, financial, social, government, geo-location, etc. This data is very valuable in terms of better understanding ourselves. Unfortunately, analyzing the data in its raw form carries the risk of exposing private information about people.

The problem of how to analyze data while protecting privacy has been around for more than 40 years---ever since the first data processing systems were developed. Most workable solutions are ad hoc: practitioners try things like removing personally identifying information (e.g. names and addresses), aggregating data, removing outlying data, and even swapping some data between individuals. This process can work reasonably well, but it is time-consuming, requires substantial expertise to get right, and invariably limits the accuracy of the analysis or the types of analysis that can be done.

A holy grail within computer science is to come up with an anonymization system that has formal guarantees of anonymity and provides good analytics. Most effort in this direction has focused on two ideas, K-anonymity and Differential Privacy. Both can provide strong anonymity, but except in rare cases neither can do so while still providing adequate analytics. As a result, common practice is still to use informal ad hoc techniques with weak anonymization, and to mitigate risk by for instance sharing data only with trusted partners.

The European Union has raised the stakes with the General Data Protection Regulation (GDPR). The GDPR has strict rules on how personal data may be used, and threatens large fines to organizations that do not follow the rules. However, GDPR says that if data is anonymous, then it is not considered personal and does not fall under the rules. Unfortunately, there are no precise guidelines on how to determine if data is anonymous or not. Member states are expected to come up with certification programs for anonymity, but do not know how to do so.

This is where we come in. Paul Francis' group, in research partnership with the startup Aircloak, has been developing an anonymizing technology called Diffix over the last five years. Diffix is an empirical, not a formal technology, and so the question remains "how anonymous is Diffix?" While it may not be possible to precisely answer that question, one way we try to answer that question is through a bounty program: we pay attackers who can demonstrate how to compromise anonymity in our system. Last year we ran the first (and still only) bounty program for anonymity. The program was successful in that some attacks were found, and in the process of designing defensive measures, Diffix has improved.

In order to run the bounty program, we naturally needed a measure of anonymity so that we could decide how much to pay attackers. We designed a measure based on how much confidence an attacker has in a prediction of an individual's data values, among other things. At some point, we realized that our measure applies not just to attacks on Diffix, but to any anonymization system. We also realized that our measure might be useful in the design of certification programs for anonymity.

We decided to develop a general score for anonymity, and to build tools that would allow anyone to apply the measure to any anonymization technology. The score is called the GDA Score, for General Data Anonymity Score.

The primary strength of the GDA Score is that it can be applied to any anonymization method, and therefore is apples-to-apples. The primary weakness is that it is based on empirical attacks (real attacks against real systems), and therefore the score is only as good as the attacks themselves. If there are unknown attacks on a system, then the score won't reflect this and may therefore make a system look more anonymous than it is.

Our hope is that over time enough attacks will be developed that we can have high confidence in the GDA Score. Towards that end, we've started the Open GDA Score Project. This is a community effort to provide software and databases in support of developing new attacks, and a repository where the scores can be viewed. We recently launched the project in the form of a website, www.gda-score.org, and some initial tools and simple attacks. We will continue to develop tools and new attacks, but our goal is to attract broad participation from the community.

For more information, visit www.gda-score.org.

We have launched the Open GDA Score Project at www.gda-score.org.  This is an open project to develop a set of tools and databases to generate anonymity scores for any data anonymization technique. The GDA Score, which stands for General Data Anonymity Score, is the first data anonymization measurement methodology that works with any anonymization technique. The GDA Score is a generalization of the measurement technique developed by Francis' group for the Diffix bounty program run last year. This was the first bounty program for anonymity. The GDA Score is of particular interest in Europe, where member states are expected to produce certification programs for anonymity.

• Bridging the Gap Between Programming Languages and Hardware Weak Memory Models by Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis.


• From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan.


• Formal verification of higher-order probabilistic programs by Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.


• Grounding Thin-Air Reads with Event Structures by Soham Chakraborty and Viktor Vafeiadis.


• On Library Correctness under Weak Memory Consistency by Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis.

What's more, the MPI-SWS Software Analysis and Verification group has a whole session to itself at POPL 2019. The weak memory session on Thursday, Jan 17, is comprised of the three papers by Viktor Vafeiadis, his students, postdocs, and collaborators.

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).

• Alan Mislove (PhD 2009) is now an Associate Professor at Northeastern University in Boston, Massachusetts, USA.


• Andreas Haeberlen (PhD 2009) is now an Associate Professor at the University of Pennsylvania in Philadelphia, Pennsylvania, USA.


• Bryan Ford (Postdoc 2009) is now an Associate Professor at EPFL in Lausanne, Switzerland.


• Meeyoung Cha (Postdoc 2010) is now an Associate Professor at KAIST in Daejon, South Korea.


• Boris Köpf (Postdoc 2010) is now a researcher at Microsoft Research Cambridge in the UK.


• Matthew Hammer (PhD 2012) is now an Assistant Professor at The University of Chicago in Illinois, USA.


• Chung-Kil Hur (Postdoc 2012) is now an Associate Professor at Seoul National University in Seoul, South Korea.


• Neel Krishnaswami (Postdoc 2012) is now a Lecturer at the University of Cambridge in the UK.


• Nuno Santos (PhD 2013) is an Assistant Professor at IST, University of Lisbon in Portugal.


• Beta Ziliani (PhD 2013) is a faculty member at Universidad Nacional de Córdoba and a researcher at CONICET in Argentina.


• Aaron Turon (Postdoc 2014) heads the the Rust Development Team at Mozilla Research. Aaron is based in Portland, Oregon, USA.


• Pedro Fonseca (PhD 2015) is an Assistant Professor at Purdue University in West Lafayette, Indiana, USA.


• Pramod Bhatotia (PhD 2015) is a Senior Lecturer at the University of Edinburgh in Scotland, UK.


• Cheng Li (PhD 2016) is a faculty member at the USTC (The University of Science and Technology of China) in Hefei, China.


• Dmitry Chistikov (Postdoc 2016) is an Assistant Professor at the University of Warwick in the UK.


• Rayna Dimitrova (Postdoc 2017) is an Assistant Professor at the University of Leicester in the UK.


• Sadegh Soudjani (Postdoc 2017) is an Assistant Professor at Newcastle University in the UK.


• Vinayak Prabhu (Postdoc 2017) is an Assistant Professor at Colorado State University in Fort Collins, Colorado, USA.


• Mainack Mondal (PhD 2017) is a faculty member at IIT Kharaghpur in West Bengal, India.


• Oana Goga (Postdoc 2017) is a researcher at CNRS in Grenoble, France.


• Riju Sen (Postdoc 2017) is an Assistant Professor at IIT Delhi in India.


• Ori Lahav (Postdoc 2017) is a Senior Lecturer at Tel Aviv University in Israel.


• Mitra Nasri (Postdoc 2018) is an Assistant Professor at the Delft University of Technology in the Netherlands.

Congratulations, everyone! We are proud that MPI-SWS alumni have spread far and wide, pursuing successful research careers all across the globe.

Georg Zetzsche has joined the institute as a tenure-track faculty member, effective November 1, 2018. He is joining us from the Institut de Recherche en Informatique Fondamentale (IRIF) at Université Paris-Diderot, where he has been a postdoctoral researcher. Georg's goal is to understand which questions about program behaviors and other infinite structures can be answered efficiently.  His research focuses on issues of decidability, complexity, synthesis, and expressiveness arising in program verification and mathematics.

Georg was previously a postdoctoral researcher in the Laboratoire Spécification et Vérification (LSV) at ENS Paris-Saclay. He obtained his PhD from the University of Kaiserslautern and his Diplom degree from Universität Hamburg. For his PhD work, Georg received the EATCS Distinguished Dissertation Award.

Applications are invited for tenure-track faculty in all areas of computer science. Pending final approval, we expect to fill one position.

A doctoral degree in computer science or related areas 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.

MPI-SWS is part of a network of over 80 Max Planck Institutes, Germany’s premier basic-research organisations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institute offers 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.

The institute is located in the German cities of Saarbruecken and Kaiserslautern, in the tri-border area of Germany, France, and Luxembourg. 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 institute.

Qualified candidates should apply on our application website (apply.mpi-sws.org). To receive full consideration, applications should be received by December 1st, 2018.

The institute is committed to increasing the representation of women and minorities, as well as of individuals with physical disabilities. We particularly encourage such individuals to apply. The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

Many real-world systems involve repeatedly making decisions under uncertainty—for instance, choosing one of the several products to recommend to a user in an online recommendation service, or dynamically allocating resources among available stock options in a financial market. Machine learning (ML) algorithms driving these systems typically operate under the assumption that they are interacting with static components, e.g., users' preferences are fixed, trading tools providing stock recommendations are static, and data distributions are stationary. This assumption is often violated in modern systems, as these algorithms are increasingly interacting with and seeking information from learning agents including people, robots, and adaptive adversaries. Consequently, many well-studied ML frameworks and algorithmic techniques fail to provide desirable theoretical guarantees—for instance, algorithms might converge to a sub-optimal solution or fail arbitrarily bad in these settings.

Researchers at the Machine Teaching Group, MPI-SWS are designing novel ML algorithms that have to interact with agents that are adaptive or learning over time, especially in situations when the algorithm's decisions directly affect the state dynamics of these agents. In recent work [1], they have studied the above-mentioned problem in the context of two fundamental machine learning frameworks: (i) online learning using experts' advice and (ii) active learning using labeling oracles. In particular, they consider a setting where experts/oracles themselves are learning agents. For instance, active learning algorithms typically query labels from an oracle, e.g., a (possibly noisy) domain expert; however, in emerging crowd-powered systems, these experts are getting replaced by inexpert participants who could themselves be learning over time (e.g., volunteers in citizen science projects). They have shown that when these experts/oracles themselves are learning agents, well-studied algorithms (like the EXP3 algorithm) fail to converge to the optimal solution and can have arbitrarily bad performance for this new problem setting. Furthermore, they provide an impossibility result showing that without sharing any information across experts, it is impossible to achieve convergence guarantees. This calls for developing novel algorithms with practical ways of coordination between the central algorithm and learning agents to achieve desired guarantees.

Currently, researchers at the Machine Teaching Group are studying these challenges in the context of designing next-generation human-AI collaborative systems. As a concrete application setting, consider a car driving scenario where the goal is to develop an assistive AI agent to drive the car in an auto-pilot mode, but giving control back to the human driver in safety-critical situations. They study this setting by casting it as a multi-agent reinforcement learning problem. When the human agent has a stationary policy (i.e., the actions take by the human driver in different states/scenarios are fixed), it is trivial to learn an optimal policy for the AI agent that maximizes the overall performance of this collaborative system. However, in real-life settings where a human driver would adapt their behavior in response to the presence of an auto-pilot mode, they show that the problem of learning an optimal policy for the AI agent becomes computationally intractable. This work is one of the recent additions to an expanding set of results and algorithmic techniques developed by MPI-SWS researchers in the nascent area of Machine Teaching [2, 3].

References

[1] Adish Singla, Hamed Hassani, and Andreas Krause. Learning to Interact with Learning Agents. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI'18), 2018.

[2] Xiaojin Zhu, Adish Singla, Sandra Zilles, and Anna N. Rafferty. An Overview of Machine Teaching. arXiv 1801.05927, 2018.

[3] Maya Cakmak, Anna N. Rafferty, Adish Singla, Xiaojin Zhu, and Sandra Zilles. Workshop on Teaching Machines, Robots, and Humans. NIPS 2017.

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.

Jonathan Mace has joined the institute as a tenure-track faculty member, effective September 1, 2018.  He is joining us from Brown University, USA, where he has completed his Ph.D. in computer science.  Jonathan's research focuses on tools, techniques, and abstractions to make it easier to develop and operate cloud distributed systems.  In particular, he is interested in making it easier to reason about and control complicated, end-to-end system behaviors at runtime.

Before starting his Ph.D., Jonathan worked for two years at IBM UK, and earned his undergraduate degree from Oxford University.  He is a recipient of the Facebook Fellowship in Distributed Systems, an SOSP Best Paper Award, and the Honorable Mention for the Dennis Ritchie Thesis Award.

Antoine Kaufmann is joining us from the University of Washington in Seattle,
where he obtained his Ph.D. in computer science. His research investigates the
design and implementation of efficient, scalable, and robust systems for
rapidly evolving modern platforms, with a current focus on data centers. He
addresses these challenges from a systems perspective, with solutions that span
multiple layers of the systems stack, from operating systems through networks
down to hardware, but also programming languages and applications.

Antoine joins the institute as a research group leader, effective Aug 6, 2018. Before
his Ph.D., Antoine obtained his Master's and Bachelor's degree from ETH Zurich.

In 1937, a young Englishman by the name of Alan M. Turing published a paper with the obscure title "On computable numbers, with an application to the Entscheidungsproblem'' in the Proceedings of the London Mathematical Society. In doing so, he arguably laid the mathematical foundations of modern computer science. Turing's seminal contribution was to show that the famous Entscheidungsproblem, formulated by the great German mathematician David Hilbert several years earlier, could not be solved: more precisely, Turing proved (in modern parlance) that the problem of determining whether a given computer program halts could not be done algorithmically---in other words that the famous Halting Problem is undecidable.

Although seemingly at the time a rather esoteric concern, the Halting Problem (and related questions) have dramatically gained in importance and relevance in more contemporary times. Fast forward to the 21st Century: nowadays, it is widely acknowledged that enabling engineers, programmers, and researchers to automatically verify and certify the correctness of the computer systems that they design is one of the Grand Challenges of computer science. In increasingly many instances, it is absolutely critical that the software governing various aspects of our daily lives (such as that running on an aircraft controller, for example) behave exactly as intended, lest catastrophic consequences ensue.

What classes of infinite-state programs can be analyzed algorithmically?

Researchers at the Foundations of Algorithmic Verification group are investigating what classes of infinite-state programs can, at least in principle, be fully handled and analyzed algorithmically by viewing computer programs abstractly as dynamical systems, and they seek to design exact algorithms enabling one to fully analyse the behaviour of such systems. In particular, they are presently tackling a range of central algorithmic problems from verification, synthesis, performance, and control for linear dynamical systems, drawing among others on tools from number theory, Diophantine geometry, and algebraic geometry, with the overarching goal of offering a systematic exact computational treatment of various important classes of dynamical systems and other fundamental models used in mathematics, computer science, and the quantitative sciences. Some of their achievements include several decidability and hardness results for linear recurrence sequences, which can be used to model simple loops in computer programs, answering a number of longstanding open questions in the mathematics and computer science literature.

In a series of recent papers [1, 2],  they have attacked the so-called Zero Problem for linear differential equations, i.e., the question of determining algorithmically whether the unique solution to a given linear differential equation has a zero or not. Such equations, which go back as far as Newton, are ubiquitous in mathematics, physics, and engineering; they are also particularly useful to model cyber-physical systems, i.e., digital systems that evolve in and interact with a continuous environment. In their work, they obtained several important partial results: if one is interested in the existence of a zero over a bounded time interval, then it is possible to determine this algorithmically, provided that a certain hypothesis from the mathematical field of number theory, known as Schanuel's Conjecture, is true. They were also able to partially account for the fact that the Zero Problem has hitherto remained open in full generality: indeed, if one were able to solve it in dimension 9 (or higher), then in turn this would enable one to solve various longstanding hard open problems from a field of mathematics known as Diophantine approximation. In doing so, they therefore exhibited surprising and unexpected connections between the modelling and analysis of cyber-physical systems and seemingly completely unrelated deep mathematical theories dealing with questions about whole numbers.

References

[1] Ventsislav Chonev, Joel Ouaknine, and James Worrell. On recurrent reachability for continuous linear dynamical systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016.

[2] Ventsislav Chonev, Joel Ouaknine, and James Worrell. On the Skolem Problem for continuous linear dynamical systems. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP), 2016.

Outstanding undergraduate and Masters students are invited to learn about world-class research in security and privacy, social systems, distributed systems, machine learning, programming languages, and verification. Leading researchers will engage with attendees in their areas of expertise: the curriculum will include lectures, projects, and interaction with faculty from participating institutions.

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 industrial research career in computer science and have a head start when applying for graduate school.

Applications are due by February 7, 2018. Travel and accommodation will be covered for accepted students.

More info can be found on the CMMRS website.

In 2018, MPI-SWS researchers authored a total of five POPL papers:

• Parametricity versus the Universal Type. Dominique Devriese, Marco Patrignani, Frank Piessens.


• Effective Stateless Model Checking for C/C++ Concurrency. Michalis Kokologiannakis, Ori Lahav, Kostis Sagonas, Viktor Vafeiadis.


• Monadic refinements for relational cost analysis. Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.


• Why is Random Testing Effective for Partition Tolerance Bugs? Rupak Majumdar, Filip Niksic.


• RustBelt: Securing the Foundations of the Rust Programming Language. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.

Furthermore, with the "RustBelt" paper, MPI-SWS faculty member Derek Dreyer cements a 10-year streak of having at least one POPL paper each year, breaking the all-time record of 9 years previously held by John Mitchell at Stanford. Congratulations Derek!

Machine learning algorithms are increasingly being used to automate decision making in several domains such as hiring, lending and crime-risk prediction. These algorithms have shown significant promise in leveraging large or “big” training datasets to achieve high prediction accuracy, sometimes surpassing even human accuracy.

Unfortunately, some recent investigations have shown that machine learning algorithms can also lead to unfair outcomes. For example, a recent ProPublica study found that COMPAS, a tool used in US courtrooms for assisting judges with crime risk prediction, was unfair towards black defendants. In fact, several studies from governments, regulatory authorities, researchers as well as civil rights groups have raised concerns about machine learning potentially acting as a tool for perpetuating existing unfair practices in society, and worse, introducing new kinds of unfairness in prediction tasks. As a consequence, a flurry of recent research has focused on defining and implementing appropriate computational notions of fairness for machine learning algorithms.

Parity-based fairness

Existing computational notions of fairness in the machine learning literature are largely inspired by the concept of discrimination in social sciences and law. These notions require the decision outcomes to ensure parity (i.e. equality) in treatment and in impact.

Notions based on parity in treatment require that the decision algorithm should not take into account the sensitive feature information (e.g., gender, race) of a user. Notions based on parity in impact require that the decision algorithm should give beneficial decision outcomes (e.g., granting a loan) to similar percentages of people from all sensitive feature groups (e.g., men, women).

However, in many cases, these existing notions are too stringent and can lead to unexpected side effects. For example, ensuring parity has been shown to lead to significant reductions in prediction accuracy. Parity may also lead to scenarios where none of the groups involved in decision making (e.g., neither men nor women) get beneficial outcomes. In other words, these scenarios might be preferred neither by the decision maker using the algorithm (due to diminished accuracy), nor by the groups involved (due to very little benefits).

User preferences and fairness

In recent work, to appear at NIPS 2017, researchers at MPI-SWS have introduced two new computational notions of algorithmic fairness: preferred treatment and preferred impact. These notions are inspired by ideas related to envy-freeness and bargaining problem in economics and game theory. Preferred treatment and preferred impact leverage these ideas to build more accurate solutions that are preferable for both the decision maker and the user groups.

The new notion of preferred treatment allows basing the decisions on sensitive feature information (thereby relaxing the parity treatment criterion) as long as the decision outcomes do not lead to envy. That is, each group of users prefers their own group membership over other groups and does not feel that presenting itself to the algorithm as another group would have led to better outcomes for the group.

The new notion of preferred impact allows differences in beneficial outcome rates for different groups (thereby relaxing the parity impact criterion) as long as all the groups get more beneficial outcomes than what they would have received under the parity impact criterion.

In their work, MPI-SWS researchers have developed a technique to ensure machine learning algorithms satisfy preferred treatment and / or preferred impact. They also tested their technique by designing crime-predicting machine-learning algorithms that satisfy the above-mentioned notions. In their experiments, they show that preference-based fairness notions can provide significant gains in overall decision-making accuracy as compared to parity-based fairness, while simultaneously increasing the beneficial outcomes for the groups involved.

This work is one of the most recent additions to an expanding set of techniques developed by MPI-SWS researchers to enable fairness, accountability and interpretability of machine learning algorithms.

References

Bilal Zafar, Isabel Valera, Manuel Gomez Rodriguez, Krishna Gummadi and Adrian Weller. From Parity to Preference: Learning with Cost-effective Notions of Fairness. Neural Information Processing Systems (NIPS), Long Beach (CA, USA), December 2017

Applications are invited for faculty positions at all career stages in computer science, with a particular emphasis on systems (broadly construed). We expect multiple positions to be filled in systems, but exceptional candidates in other areas of computer science are also strongly encouraged to apply.

A doctoral degree in computer science or related areas and an outstanding research record (commensurate for the applicant's career stage) 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.

MPI-SWS is part of a network of over 80 Max Planck Institutes, Germany's premier basic-research organisations. MPIs have an established record of world-class, foundational research in the sciences, technology, and the humanities. The institute offers 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.

The institute is located in the German cities of Saarbruecken and Kaiserslautern, in the tri-border area of Germany, France, and Luxembourg. 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 institute.

Qualified candidates should apply on our application website (apply.mpi-sws.org). To receive full consideration, applications should be received by December 1st, 2017.

The institute is committed to increasing the representation of minorities, women, and individuals with physical disabilities. We particularly encourage such individuals to apply. The initial tenure-track appointment is for five years; it can be extended to seven years based on a midterm evaluation in the fourth year. A permanent contract can be awarded upon a successful tenure evaluation in the sixth year.

MPI-SWS faculty member Derek Dreyer has received the 2017 Robin Milner Young Researcher Award, which is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages.  The award citation reads as follows:

"Derek Dreyer has made deep, creative research contributions of great breadth. His areas of impact are as diverse as module systems, data abstraction in higher-order languages, mechanized proof systems and techniques, and concurrency models and semantics. He has refactored and generalized the complex module systems of SML and OCaml; devised logical relations and techniques that enabled advances in reasoning about higher-order imperative programs; and developed novel separation logics for modular verification of low-level concurrent programs. His research papers are a model of clarity and depth, and he has worked actively to translate his foundational ideas into practice – most recently with the RustBelt project to provide formal foundations for the Rust language. Additionally, Dreyer has contributed leadership, support, and mentorship in activities such as the PLMW series of workshops, which are instrumental in growing the next generation of PL researchers."

Previous recipients of the award have included Stephanie Weirich, David Walker, Sumit Gulwani, Lars Birkedal, and Shriram Krishnamurthi.

Amaury Pouly, a postdoc in Joël Ouaknine's Foundations of Automatic Verification Group, has received the 2017 Ackermann Award for his PhD thesis, “Continuous-time computation models: From computability to computational complexity.” The Ackermann Award is an international prize presented annually to the author of an exceptional doctoral dissertation in the field of Computer Science Logic.

Amaury Pouly's thesis shows that problems which can be solved with a computer in a reasonable amount of time (more specifically problems which belong to the class P of the famous open problem “P = NP?”) can be characterized as polynomial length solutions of polynomial differential equations. This result paves the way for reformulating certain questions and concepts of theoretical computer science in terms of ordinary polynomial differential equations. It also revisits analog computational models and demonstrates that analog and digital computers actually have the same computing power, both in terms of what they can calculate (computability) and what they can solve in reasonable (polynomial) time.

MPI-INF and MPI-SWS jointly participated in Girl's Day this year.

The Max Planck Institutes for Informatics and Software Systems pursue basic research in many areas of computer science. But what exactly is computer science? And what does a day in the life of a scientist look like in computer science? We addressed these questions by way of hands-on examples and demonstrated, for instance, how a computer learns, how the car navigation system knows how to get from A to B, and also how one doesn’t always need a computer for doing computer science. Along the way, the school girls were able to ask our students and researchers all sorts of questions about what it is like to work in research.

--------

Die Max-Planck Institute für Informatik und Software Systeme betreiben Grundlagenforschung in vielen Bereichen der Informatik. Aber was genau ist Informatik? Und wie sieht ein Tag im Leben einer Wissenschaftlerin in der Informatik aus? Genau dies haben wir anhand von Beispielen zum Anfassen und Ausprobieren gezeigt und dabei z.B. illustriert, wie ein Computer lernt, wie das Navi weiß wie man von A nach B kommt, und auch dass man für Informatik nicht immer einen Computer braucht. Nebenbei hatten die Schülerinnen die Gelegenheit unseren StudentInnen, DoktorandInnen und WissenschaftlerInnen allerlei Fragen zu stellen, wie es denn ist in der Forschung zu arbeiten.

Outstanding undergraduate and Masters students are invited to learn about world-class research in security and privacy, social systems, distributed systems, machine learning, programming languages, and verification. Leading researchers will engage with attendees in their areas of expertise: the curriculum will include lectures, projects, and interaction with faculty from participating institutions.

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 industrial research career in computer science and have a head start when applying for graduate school.

Applications are due by February 7, 2017. Travel and accommodation will be covered for accepted students.

More info can be found on the CMMRS website.

MPI-SWS offers a vibrant, dynamic, multi-cultural environment for research and education. We have openings for both graduate students and postdoctoral research scholars.

Graduate students work as members of one or more of the institute's research groups, which perform internationally leading, highly visible research in their respective fields of specialization. Graduate students receive individual training and mentorship from MPI-SWS faculty, preparing them for leadership positions in academic or industrial research.

Postdoctoral Fellows have the opportunity to work with MPI-SWS faculty on existing lines of research, as well as develop their own research agenda under MPI-SWS faculty supervision.

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

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

Joel Ouaknine joins the institute's faculty as a scientific director, effective Aug 1, 2016. Joel's research interests include the automated verification of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, synthesis problems, complexity), logic and applications to verification, decision and synthesis problems for linear dynamical systems, automated software analysis, concurrency, and theoretical computer science.

In 2015, Joel was awarded an ERC Consolidator Grant, which provides almost 2 million euros of research funding over a period of five years. He is also the recipient of the 2010 Roger Needham Award, given annually "for a distinguished research contribution in Computer Science by a UK-based researcher within ten years of his or her PhD."

Joel will join MPI-SWS from the University of Oxford, where he is a Professor of Computer Science and Fellow of St John's College. Joel holds a BSc and MSc in Mathematics from McGill University, and received his PhD in Computer Science from Oxford in 2001. He subsequently did postdoctoral work at Tulane University and Carnegie Mellon University.