News 2018

Five MPI-SWS papers at POPL 2019!

December 2018
Just as in 2018, MPI-SWS researchers again authored a total of five POPL papers in 2019:
  • 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.

MPI-SWS alumni in leadership positions

November 2018
Since its founding at the end of 2004, MPI-SWS has been fortunate to have been the academic home of many amazing doctoral students and postdoctoral fellows. With the ten-year anniversary of the graduation of our first students coming up soon, we wanted to take a moment to celebrate some of the achievements of our alumni:
  • 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 now an Assistant Professor at IST, University of Lisbon in Portugal.
  • Aaron Turon (Postdoc 2014) now heads the the Rust Development Team at Mozilla Research. Aaron is based in Portland, Oregon, USA.
  • Pedro Fonseca (PhD 2015) is now an Assistant Professor at Purdue University in West Lafayette, Indiana, USA.
  • Pramod Bhatotia (PhD 2015) is now a Senior Lecturer at the University of Edinburgh in Scotland, UK.
  • Cheng Li (PhD 2016) is now 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 joins MPI-SWS

November 2018
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.

Jonathan Mace receives Dennis M. Ritchie Dissertation Honorable Mention

October 2018
MPI-SWS faculty member Jonathan Mace has received an honorable mention for the Dennis M. Ritchie Doctoral Dissertation Award.

Launched in 2013, the Dennis M. Ritchie Doctoral Dissertation Award was created by the Association for Computing Machinery's Special Interest Group on Operating Systems (ACM SIGOPS) to recognize research in software systems and to encourage the creativity that Dennis Ritchie embodied. Only one winner is chosen annually, and this year, Jonathan Mace's dissertation received an Honorable Mention for the award.

"Many tools for monitoring and enforcing distributed systems," Jonathan explains, "capture information about end-to-end executions by propagating in-band contexts." In his thesis---A Universal Architecture for Cross-Cutting Tools in Distributed Systems"---he characterizes a broad class of such cross-cutting tools and extends these ideas to new applications in resource management and dynamic monitoring. Finally, he identifies underlying commonalities in this class of tools, and proposes an abstraction layering that simplifies their development, deployment, and reuse.

Tenure-Track Faculty Position

October 2018
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.

Research Spotlight: Learning to interact with learning agents

September 2018
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 awarded ERC Advanced Grant

September 2018
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 joins MPI-SWS

September 2018
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 joins MPI-SWS

August 2018
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.

MPI-SWS and MPI-INF jointly participated in the 2018 Girls' Day

June 2018
For the second year in a row, the MPIs for Informatics and Software Systems
jointly participated in the annual Girls' Day. We welcomed 14 school-aged girls to
our institute, and showed them what computer science research is all about. We
spent an exciting morning with hands-on computer science puzzles, soldered
cool blinking hearts, and live-edited videos. The winners of our computer science
quiz got to take home 3D dragons, printed on our own 3D printers.

Research Spotlight: From Newton to Turing to cyber-physical systems

February 2018
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.

Björn Brandenburg receives SIGBED Early Career Award

February 2018
MPI-SWS faculty member Björn Brandenburg has received the first ever SIGBED Early Career Researcher Award. The award is given by ACM SIGBED to recognize outstanding contributions by young investigators in the area of embedded, real-time, and cyber-physical systems.

A week-long school for outstanding undergrad/MS students curious about research in computing. Apply now!

January 2018
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.

POPLpalooza: Five MPI-SWS papers at POPL 2018 + a new record!

January 2018
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!

Research Spotlight: Teaching machine learning algorithms to be fair

January 2018
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