News

MPI-SWS PhD students appointed as tenure-track faculty at ETH Zurich and ISTA

December 2023
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, ...
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!
Read more

Francis' group releases SynDiffix, the world's most accurate synthetic data generator

December 2023
Paul Francis's Open Diffix project has released SynDiffix, an open-source Python package that generates statistically accurate, privacy preserving synthetic data from structured data. Using SynDiffix, a data owner can safely share data while retaining most of the statistical properties of the original data. Analysts can work with the synthetic data as though it were the original.

Using the novel techniques of sticky noise and range snapping, ...
Paul Francis's Open Diffix project has released SynDiffix, an open-source Python package that generates statistically accurate, privacy preserving synthetic data from structured data. Using SynDiffix, a data owner can safely share data while retaining most of the statistical properties of the original data. Analysts can work with the synthetic data as though it were the original.

Using the novel techniques of sticky noise and range snapping, SynDiffix breaks new ground in data accuracy. It is 10 to 100 times more accurate than the open source tool CTGAN, and 5 to 10 times more accurate than the best commercial synthetic data generators. This makes SynDiffix particularly well suited to descriptive analytics like histograms, heatmaps, averages and standard deviations, column correlations, and so on. Like other tools, however, it can also be used for ML modeling. Francis is hopeful that SynDiffix will find wide practical use as well as motivate more research on synthetic data.
Read more

Anne-Kathrin Schmuck joins MPI-SWS tenure-track faculty

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-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.
Read more

MPI-SWS alumnus Pramod Bhatotia receives EuroSys Jochen Liedtke Young Researcher Award

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. ...
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!
Read more

MPI-SWS researchers receive the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

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,
...
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: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.
Read more

Kaushik Mallik awarded ETAPS Doctoral Dissertation 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. ...
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.
Read more

Georg Zetzsche awarded ERC Starting Grant

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". ...
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.
Read more

Laurent Bindschaedler joins MPI-SWS faculty

November 2022
Laurent Bindschaedler joins the faculty as a Research Group Leader at our institute starting November 2022. Laurent will be heading the Data Systems Group (DSG), which is focused on exploring a wide range of topics at the intersection of systems, data management, and machine learning. His group is particularly interested in systems for big data and machine learning, machine learning for systems, real-time analytics systems, and decentralized systems.

Before joining MPI-SWS, Laurent was a postdoctoral researcher at MIT CSAIL, ...
Laurent Bindschaedler joins the faculty as a Research Group Leader at our institute starting November 2022. Laurent will be heading the Data Systems Group (DSG), which is focused on exploring a wide range of topics at the intersection of systems, data management, and machine learning. His group is particularly interested in systems for big data and machine learning, machine learning for systems, real-time analytics systems, and decentralized systems.


Before joining MPI-SWS, Laurent was a postdoctoral researcher at MIT CSAIL, working with Prof. Tim Kraska. He completed his Ph.D. at EPFL, advised by Prof. Willy Zwaenepoel. Laurent built the Chaos graph processing system, which holds a record for the largest graph processed in a small cluster of commodity servers. He is the recipient of a Swiss National Science Foundation Fellowship from 2020 to 2022 and an EPFL EDIC Fellowship from 2015 to 2016.


Laurent’s personal website: https://binds.ch

Read more

Tenure-track Openings at Max Planck Institutes in Computer Science

November 2022
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, ...
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.
Read more

Ralf Jung accepts faculty position at ETH Zurich

October 2022
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.. ...
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/.
Read more

Mariya Toneva joins MPI-SWS tenure-track faculty

September 2022
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. ...
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.
Read more

Rupak Majumdar wins CONCUR test-of-time award

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


 

Read more

Viktor Vafeiadis receives Robin Milner Young Researcher Award

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, ...
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.
Read more

Two faculty win prestigious Google Research Scholar awards

June 2022

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

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.
Read more

Derek Dreyer appointed MPI-SWS Director

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, ...
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.
Read more

Sandra Kiefer joins MPI-SWS

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. ...
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.
Read more

Outstanding Paper Honorable Mention at AAAI 2022

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. ...
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.
Read more

Joël Ouaknine appointed ACM Fellow

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, ...
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: 
Read more

Bob Harper receives ACM SIGPLAN Achievement Award

January 2022
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, ...
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.”
Read more

Adish Singla awarded ERC Starting Grant

January 2022
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, ...
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.
Read more

Goran Radanovic receives Emmy Noether Award

January 2022


Goran Radanovic, a research group leader in the Multi-Agent Systems 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.

Goran's group will be hosted at MPI-SWS in Saarbruecken and will contribute to research on reinforcement learning for multi-agent systems. ...


Goran Radanovic, a research group leader in the Multi-Agent Systems 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.

Goran's group will be hosted at MPI-SWS in Saarbruecken and will contribute to research on reinforcement learning for multi-agent systems. His Emmy Noether research project will focus on designing a framework for trustworthy multi-agent sequential decision making, and will study two important aspects of trustworthiness: robustness (the ability to deal with adversaries and uncertainty) and accountability (the ability to provide an account for one’s behavior).

Read more

Max Planck researchers publish 11 papers at POPL 2022!

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!
...
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!
Read more

Tenure-track Openings at Max Planck Institutes in Computer Science

November 2021
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, ...
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.
Read more

Antoine Kaufman joins MPI-SWS tenure-track faculty

October 2021
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 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.
Read more

MPI-SWS students receive ACM SIGPLAN Dissertation Award two years in a row

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. ...
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.
Read more

Ralf Jung receives ACM Doctoral Dissertation Award Honorable Mention

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 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.
Read more

Arpan Gujarati receives 2021 ACM SIGBED Paul Caspi Memorial Dissertation Award

Arpan Gujarati's thesis, entitled  Towards “Ultra-Reliable" CPS: Reliability Analysis of Distributed Real-Time Systems, has been recognized with the 2021 ACM SIGBED Paul Caspi Memorial Dissertation Award. The award, first given in 2013, recognizes outstanding doctoral dissertations that significantly advance the state of the art in the science of embedded systems, in the spirit and legacy of Dr. Paul Caspi’s work. Arpan was advised by MPI-SWS faculty member Björn Brandenburg.

Otto Hahn Medal awarded to two MPI-SWS students

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 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.
Read more

Girls' Day 2021

April 2021
MPI-SWS participated jointly with the MPI for Informatics in the annual Girls' Day event on April 22, 2021. Our interactive digital program
included  programming robots and integrating machine learning models into dialog systems, as well as answering questions about computer
science and the work as a computer scientist.

ETAPS dissertation award and CACM article for Ralf Jung and his work on Rust

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

Read more

Max Planck researchers publish 8 papers at POPL 2021!

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! ...
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:

MPI-SP papers:
Read more

Viktor Vafeiadis awarded ERC Consolidator Grant

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

Read more

Filip Niksic awarded ACM SIGPLAN John C. Reynolds Dissertation Award

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. ...
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.
Read more

Joël Ouaknine is a co-recipient of the 2020 Salomaa prize

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

 
Read more

Tenure-track Openings at Max Planck Institutes in Computer Science

November 2020
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, ...
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.
Read more

Research Spotlight: Steering Policies in Multi-Agent Collaboration

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. ...
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.
Read more

Joël Ouaknine elected member of Academia Europaea

MPI-SWS faculty member Joël Ouaknine has been elected a member of the Academia Europaea in 2020.  This is the second election for MPI-SWS, following the election of Peter Druschel as a member in 2008.

The aim of the Academy is to promote European research, advise governments and international organisations in scientific matters, and further interdisciplinary and international research.

More information: Joel's Academia Europaea page and the list of all members elected in 2020

Manuel Gomez-Rodriguez awarded ERC Starting Grant

September 2020
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, ...
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.
Read more

Anne-Kathrin Schmuck receives Emmy Noether Award

September 2020
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. ...
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.
Read more

Aastha Mehta accepts faculty position at University of British Columbia

September 2020
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/.
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/.
Read more

Max Planck researchers publish 17 papers at LICS/ICALP 2020

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

Read more

Research Spotlight: Software Engineering for Machine Learning

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, ...
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.
Read more

Research Spotlight: Logic and Learning

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 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
Read more

Max Planck researchers publish 8 papers at POPL 2020 + a new record!

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

Read more

Tenure-track Openings at Max Planck Institutes in Computer Science

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 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.
Read more

Goran Radanovic joins MPI-SWS

September 2019
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. ...
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.
Read more

Filip Mazowiecki joins MPI-SWS

September 2019
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, ...
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.
Read more

Paper by MPI-SWS researchers wins both a 2019 Usenix Security Symposium Distinguished Paper Award and the Usenix/Facebook Internet Defense Prize

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 "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.
Read more

Keon Jang joins MPI-SWS

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, ...
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.
Read more

Krishna Gummadi appointed MPI-SWS Director

Krishna Gummadi has accepted the position of scientific member of the Max Planck Society and director at the MPI for Software Systems, effective 1 June 2019. Krishna has been a faculty member at the institute since July 2005. 

Krishna's appointment solidifies our institute's foothold in the emerging area of social computing and secures Krishna's leadership and contributions to the institute for the future.

Research Spotlight: Tracing the Behavior of Cloud Applications

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, ...
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.
Read more

Girls' Day 2019

April 2019
As in the years before, the MPIs for Informatics and Software Systems jointly participated in the annual Girls' Day on 28 March. We welcomed a record number of 27 school-aged girls to our institutes to provide them with a bit of insight into computer science. Together we programmed smartphone apps, soldered blinking smiles and running bugs, and solved hands-on computer science puzzles.

Research Spotlight: A General Data Anonymity Measure

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. ...
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.
Read more

Francis' group launches Open GDA Score Project

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. ...
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.
Read more

Five MPI-SWS papers at POPL 2019!

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,
...
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.
Read more

ERC-supported TOROS Project officially launches!

January 2019
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),  ...
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).
Read more

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,
...
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 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.
Read more

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. ...
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.
Read more

Tenure-Track Faculty Position

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, ...
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.
Read more

Research Spotlight: Learning to interact with learning agents

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, ...
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.
Read more

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. ...
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.
Read more

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 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.
Read more

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, ...
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.
Read more

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

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, ...
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.
Read more

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, ...
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.
Read more

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

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,
...
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!
Read more

Maria Christakis receives Facebook Faculty Research Award

December 2017
Maria Christakis, an MPI-SWS faculty member, has received a Facebook Faculty Research Award. The award is given in recognition of Maria's work on combining static and dynamic program analysis, which is of particular relevance to Facebook as they are developing sophisticated program analysis tools to handle real-world code.

Research Spotlight: Teaching machine learning algorithms to be fair

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,

...
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
Read more

Multiple Tenure-Track Faculty Openings

September 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, ...
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.
Read more

Derek Dreyer receives Robin Milner Young Researcher Award

September 2017
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. ...
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.
Read more

Amaury Pouly receives Ackermann Award

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. ...
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.
Read more

Adish Singla to join MPI-SWS as tenure-track faculty



Adish Singla is joining us from ETH Zurich, where he has completed his Ph.D. in computer science. His research focuses on designing new machine learning frameworks and developing algorithmic techniques, particularly for situations where people are an integral part of computational systems. Adish joins the institute as a tenure-track faculty member, effective Oct 1, 2017.

Before starting his Ph.D., he worked as a Senior Development Lead in Bing Search for over three years. ...


Adish Singla is joining us from ETH Zurich, where he has completed his Ph.D. in computer science. His research focuses on designing new machine learning frameworks and developing algorithmic techniques, particularly for situations where people are an integral part of computational systems. Adish joins the institute as a tenure-track faculty member, effective Oct 1, 2017.

Before starting his Ph.D., he worked as a Senior Development Lead in Bing Search for over three years. Adish received his Bachelor's degree from IIT Delhi and his Master's degree from EPFL. He is a recipient of the Facebook Fellowship in the area of Machine Learning, the Microsoft Research Tech Transfer Award, and the Microsoft Gold Star Award.

Read more

Peter Druschel receives EuroSys Lifetime Achievement Award

Peter Druschel has received the 2017 EuroSys Lifetime Achievement Award for his numerous and valuable contributions to research in computer systems. It is the highest honor accorded by EuroSys to systems researchers.

Real-Time Systems group receives 3 best-paper awards in a row

The MPI-SWS Real-Time Systems group, led by Björn Brandenburg, has won the best paper award at ECRTS’16, the best paper award at RTSS’16, and the best paper award at RTAS’17. These are the three main conferences in real-time systems.  This is the first time a group has won best paper awards in all three consecutive top real-time systems conferences. Congratulations to Björn and the postdocs and students in the real-time systems group!

Girls' Day 2017

March 2017
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, ...
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.
Read more

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

January 2017
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, ...
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.
Read more

Join us! Applications invited for doctoral and post-doctoral positions

November 2016
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, ...
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.
Read more

Max Planck Society Seeks Nominations for Scientific Directors

November 2016
The Max Planck Society  seeks nominations  for scientific directors in several research fields, including Computer Science. Nominations should be received by Dec 12, 2016.

Multiple Tenure-Track Faculty Openings

Applications are invited for tenure-track faculty positions in all areas related to the theory and practice of software systems, including security and privacy, embedded and mobile systems, distributed and parallel systems, computational social science, legal, economic, and social aspects of computing, NLP, machine learning, information and knowledge management, programming languages, algorithms and logic, and verification.

To receive full consideration, applications should be received by December 15, 2016. For further details see our job ad.

Peter Druschel recognized as a Microsoft Outstanding Collaborator

MPI-SWS Director Peter Druschel was honored with a Microsoft Outstanding Collaborator Award. The award was given for his numerous contributions to Microsoft Research over the years. Druschel's collaborative work with Microsoft Research has generated a long stream of seminal papers. One of the most noteworthy is his paper on the distributed hash table Pastry --- a paper that is one of the most highly cited papers ever written by MSR researchers.

Derek Dreyer awarded ERC Consolidator Grant

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, ...
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
Read more

Announcing the Maryland Max Planck Ph.D. Program in Computer Science

We are pleased to announce the formation of The Maryland Max Planck Ph.D. Program in Computer Science. This program offers students a unique opportunity to pursue a Ph.D. degree under the supervision of faculty from the University of Maryland, USA, and a Max Planck Institute in Germany. Students are co-advised, perform collaborative research, take advantage of the expertise, resources, and culture at both institutions, and spend time in both countries.

Joel Ouaknine joins the MPI-SWS faculty

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. ...
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.
Read more

Sadegh Soudjani receives DIC Best PhD-Thesis Award

MPI-SWS postdoctoral fellow Sadegh Soudjani has been awarded the DISC Best PhD-Thesis Award for the best PhD thesis defended in 2014 in the Netherlands in the area of systems and control. Dr. Soudjani received the award for the excellent quality of his PhD Thesis "Formal Abstraction for Automated Verification and Synthesis of Stochastic Systems" for which he obtained the doctoral degree at Delft University of Technology in November.

Isabel Valera and Rijurekha Sen awarded Humboldt fellowships

MPI-SWS postdoctoral fellows Isabel Valera and Rijurekha Sen have each received a two-year Humboldt postdoctoral fellowship. The fellowship enables highly-qualified scientists from abroad to spend extended periods of research in Germany. Dr. Valera recently joined the newly created Learning in Networks research group and Dr. Sen collaborates with both the MPI-SWS Distributed Systems and Social Computing research groups.

Rijurekha Sen receives ACM-India Doctoral Dissertation Award

MPI-SWS postdoctoral fellow Rijurekha won the 2014 Best Doctoral Dissertation Award by ACM-India for her thesis titled "Different Sensing Modalities for Traffic Monitoring in Developing Regions" Dr. Sen recently joined the MPI-SWS Distributed Systems and Social Computing research groups.

MPI-SWS spinoff Aircloak wins Cisco IoT Security Grand Challenge

MPI-SWS spinoff Aircloak has won the 2014 Cisco Internet of Things (IoT) Security Grand Challenge. Aircloak was selected for its innovative approach to privacy protection—it is building the world's first anonymized analytics system. As a grand challenge award winner, Aircloak was awarded a $75,000 cash prize and was showcased at the IoT World Forum. In addition, the award also provides the Aircloak team with mentoring, training and access to business expertise from Cisco and other supporting organizations, ...
MPI-SWS spinoff Aircloak has won the 2014 Cisco Internet of Things (IoT) Security Grand Challenge. Aircloak was selected for its innovative approach to privacy protection—it is building the world's first anonymized analytics system. As a grand challenge award winner, Aircloak was awarded a $75,000 cash prize and was showcased at the IoT World Forum. In addition, the award also provides the Aircloak team with mentoring, training and access to business expertise from Cisco and other supporting organizations, as well as potential investment and partnering opportunities in the future. For more info see the Cisco award announcement (in English or in German), and the Cisco blog.
Read more

Aaron Turon receives SIGPLAN Dissertation Award

Aaron Turon, a postdoc in Derek Dreyer's Foundations of Programming Group, has received the 2014 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award for his PhD thesis, "Understanding and Expressing Scalable Concurrency", which he completed at Northeastern University in 2013 under the supervision of Mitch Wand. This international award is presented annually to the author of the outstanding doctoral dissertation in the area of Programming Languages. Aaron has recently joined Mozilla Research in San Francisco, ...
Aaron Turon, a postdoc in Derek Dreyer's Foundations of Programming Group, has received the 2014 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award for his PhD thesis, "Understanding and Expressing Scalable Concurrency", which he completed at Northeastern University in 2013 under the supervision of Mitch Wand. This international award is presented annually to the author of the outstanding doctoral dissertation in the area of Programming Languages. Aaron has recently joined Mozilla Research in San Francisco, where he is a member of the development team for the Rust programming language.
Read more

Rupak Majumdar receives Most Influential Paper Award

MPI-SWS faculty member Rupak Majumdar has been selected as the winner of this year's POPL (Principles of Programming Languages) Most Influential Paper Award. The ACM SIGPLAN Most Influential POPL Paper Award is a retrospective award—it is given each year to the paper deemed most influential from the POPL conference 10 years earlier.

Majumdar won the award for his 2004 paper, Abstractions From Proofs, which was coauthored with Thomas Henzinger, Ranjit Jhala, and Kenneth McMillan. ...
MPI-SWS faculty member Rupak Majumdar has been selected as the winner of this year's POPL (Principles of Programming Languages) Most Influential Paper Award. The ACM SIGPLAN Most Influential POPL Paper Award is a retrospective award—it is given each year to the paper deemed most influential from the POPL conference 10 years earlier.

Majumdar won the award for his 2004 paper, Abstractions From Proofs, which was coauthored with Thomas Henzinger, Ranjit Jhala, and Kenneth McMillan. The paper introduced a technique to automatically find program abstractions using logical interpolation and showed the effectiveness of the technique in software verification.
Read more

MPI-SWS featured in local documentary

MPI-SWS was featured in a documentary produced by local public broadcasting company SWR Rheinland-Pfalz. Part of the "Made in Rheinland-Pfalz" series, the documentary focuses on three software organizations along the "Software Mile" in Kaiserslautern: MPI-SWS, The Fraunhofer IESE, and DFKI. The documentary includes a brief interview with MPI-SWS faculty member Björn Brandenburg and research scientist Felix Bauer.

The documentary will be aired on January 22 at 6:15 pm.

MPI-SWS researchers awarded ERC Synergy Grant

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

Over the next six years their project "imPACT: Privacy, Accountability, Compliance, and Trust in Tomorrow's Internet" will receive almost 10 million euros, which will allow them to explore how to protect users against eavesdropping and fraud on the Internet without restricting trade, ...
MPI-SWS directors Peter Druschel and Rupak Majumdar, along with Gerhard Weikum (Scientific Director at the MPI for Informatics) and Michael Backes (MPI-SWS Fellow and Professor at Saarland University), have jointly been awarded the prestigious ERC Synergy Grant.

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

MPI-SWS student receives Google Scholarship

MPI-SWS PhD student Juhi Kulshrestha was awarded a Google Anita Borg Scholarship. She joins Ezgi Cicek, who received an Anita Borg Scholarship in 2012. Juhi previously received a 2011 Google Fellowship for her work in social networking.

Cristian Danescu-Niculescu-Mizil wins WWW best paper award

MPI-SWS faculty member Cristian Danescu-Niculescu-Mizil, along with his co-authors, has won the 2013 WWW Best Paper Award for his paper "No Country for Old Members: User Lifecycle and Linguistic Change in Online Communities."

Derek Dreyer wins funding from Microsoft Research

May 2013
A research project proposed by MPI-SWS faculty member Derek Dreyer has been selected for a 2013 Microsoft Research PhD Scholarship. The project is entitled "Compositional Verification of Scalable Joins by Protocol-Based Refinement". Each year Microsoft selects approximately twenty projects to fund, based on proposals from research institutions across Europe, Africa, and the Middle East. The Scholarship funds a PhD student for three years.

Björn Brandenburg receives EDAA dissertation award

MPI-SWS faculty member Björn Brandenburg has won the 2012 EDAA Outstanding Dissertations Award in the category "New directions in embedded system design and embedded software", to be presented at the DATE 2013 conference in March. This marks the third award Brandenburg has received for his dissertation.

Björn Brandenburg receives North American dissertation award

Björn Brandenburg, an MPI-SWS faculty member, has been awarded the Council of Graduate Schools/ProQuest Distinguished Dissertation Award in the area of mathematics, physical sciences, and engineering. The award—North America's most prestigious honor for doctoral dissertations—recognizes recent doctoral recipients who have already made unusually significant and original contributions to their fields.

Brandenburg's dissertation, "Scheduling and Locking in Multiprocessor Real-Time Operating Systems," was also selected for the 2012 Linda Dykstra Distinguished Dissertation Award, ...
Björn Brandenburg, an MPI-SWS faculty member, has been awarded the Council of Graduate Schools/ProQuest Distinguished Dissertation Award in the area of mathematics, physical sciences, and engineering. The award—North America's most prestigious honor for doctoral dissertations—recognizes recent doctoral recipients who have already made unusually significant and original contributions to their fields.

Brandenburg's dissertation, "Scheduling and Locking in Multiprocessor Real-Time Operating Systems," was also selected for the 2012 Linda Dykstra Distinguished Dissertation Award, which recognizes the best dissertation among all graduates in the fields of mathematics, physical sciences, and engineering at the University of North Carolina at Chapel Hill.
Read more

Visiting Professor Lorenzo Alvisi receives Humboldt Award

Lorenzo Alvisi, a professor at the University of Texas at Austin, has been selected for a prestigious Humboldt Research Award from the Alexander von Humboldt Foundation. This award provides support for him to spend up to a year at the institute, where he will work with Peter Druschel and other MPI-SWS researchers on fault-tolerant computing for multi-core servers.

This is the second year that an MPI-SWS visiting professor has received a Humboldt Award. ...
Lorenzo Alvisi, a professor at the University of Texas at Austin, has been selected for a prestigious Humboldt Research Award from the Alexander von Humboldt Foundation. This award provides support for him to spend up to a year at the institute, where he will work with Peter Druschel and other MPI-SWS researchers on fault-tolerant computing for multi-core servers.

This is the second year that an MPI-SWS visiting professor has received a Humboldt Award. Johannes Gehrke was a 2010 Humboldt Research Award recipient.

The Humboldt Research Award is granted "in recognition of a researcher's entire achievements to date to academics whose fundamental discoveries, new theories, or insights have had a significant impact on their own discipline and who are expected to continue producing cutting-edge achievements in the future."
Read more