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!

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

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

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

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

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

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

Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 6 papers accepted to POPL 2023.  This is the sixth year in a row that MPI-SWS researchers have published 5+ papers in POPL.  Furthermore, one Max Planck paper was awarded a 2023 POPL Distinguished Paper Award. Congratulations to all our POPL authors!

• Conditional Contextual Refinement by Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer


• Context-Bounded Verification of Context-Free Specifications by Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche


• DimSum: A Decentralized Approach to Multi-language Semantics and Verification by Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer.  DISTINGUISHED PAPER


• Kater: Automating Weak Memory Model Metatheory and Consistency Checking by Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis


• The Path to Durable Linearizability by Emanuele D’Osualdo, Azalea Raad, Viktor Vafeiadis


• CoqQ: Foundational Verification of Quantum Programs by Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying