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

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


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


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


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


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


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


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


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


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


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


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

Sumit Gulwani, a scientist at Microsoft Research in Redmond, is one of two recipients of the 2021 Max Planck-Humboldt Medal. He will collaborate with MPI-SWS faculty Rupak Majumdar and Adish Singla on the problem of AI in Education.

With a background in program analysis and artificial intelligence, Sumit Gulwani shaped the field of program synthesis, which emerged around 2010. The computer scientist developed algorithms that can efficiently generate computer programs from very few input-output examples, natural-language-based specification, or from just the code and data context. His work made it possible for non-programmers to program tedious, repetitive spreadsheet tasks, and enabled productivity improvements for data scientists and developers for data wrangling and software engineering tasks. Recently, Sumit has also been using the tools of program synthesis for computer-aided education of pupils and students. Starting from the automatic correction of learners' work in programming education, he further evolved this line of work to detect misunderstandings and give learning feedback and grades, also in subjects like mathematics and language learning.

The medal comes with prize money in the amount of 60,000 euros.

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

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

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

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

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

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

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

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

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

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

MPI-SWS papers:

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


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


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


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


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


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

MPI-SP papers:

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


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