• 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!