News 2025

Programming Languages & Verification

Derek Dreyer and collaborators receive three Distinguished Paper Awards at PLDI'25 and POPL'25

MPI-SWS faculty member Derek Dreyer and his collaborators made a very strong showing at the top programming language conferences this year.  They received Distinguished Paper Awards for two papers at PLDI 2025 and one at POPL 2025.  At PLDI this year, only 6 papers were given this award out of 89 accepted papers. At POPL this year, only 7 papers were given this award out of 81 accepted papers.

Tree Borrows
by Neven Villani, ...
MPI-SWS faculty member Derek Dreyer and his collaborators made a very strong showing at the top programming language conferences this year.  They received Distinguished Paper Awards for two papers at PLDI 2025 and one at POPL 2025.  At PLDI this year, only 6 papers were given this award out of 89 accepted papers. At POPL this year, only 7 papers were given this award out of 81 accepted papers.


Tree Borrows
by Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
PLDI 2025
https://dl.acm.org/doi/10.1145/3735592
Destabilizing Iris
by Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer
PLDI 2025
https://dl.acm.org/doi/10.1145/3729284
Data Race Freedom à la Mode
by Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer
POPL 2025
https://dl.acm.org/doi/10.1145/3704859


Read more

Michael Sammler receives Otto Hahn Medal

Michael Sammler has been awarded the 2024 Otto Hahn Medal.  The Max Planck Society awards the Otto Hahn Medal annually to young scientists in recognition of outstanding scientific achievement. Michael was awarded the medal for his PhD dissertation, entitled "Automated and Foundational Verification of Low-Level Programs".  Michael obtained his PhD in 2023, and was advised by Deepak Garg and Derek Dreyer. Michael subsequently did a postdoc at ETH Zurich with Peter Müller, and is now tenure-track faculty at IST Austria. ...
Michael Sammler has been awarded the 2024 Otto Hahn Medal.  The Max Planck Society awards the Otto Hahn Medal annually to young scientists in recognition of outstanding scientific achievement. Michael was awarded the medal for his PhD dissertation, entitled "Automated and Foundational Verification of Low-Level Programs".  Michael obtained his PhD in 2023, and was advised by Deepak Garg and Derek Dreyer. Michael subsequently did a postdoc at ETH Zurich with Peter Müller, and is now tenure-track faculty at IST Austria.


 
Read more

Derek Dreyer receives most influential POPL paper award

MPI-SWS faculty member Derek Dreyer and his collaborators (including MPI-SWS alumni Ralf Jung, David Swasey, and Aaron Turon) have received the 2025 Most Influential POPL Paper Award for their POPL 2015 paper, "Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning" (https://iris-project.org/pdfs/2015-popl-iris1-final.pdf).  This comes on top of the Alonzo Church Award that they received in 2023 for the four core papers on the foundations of Iris.

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. ...
MPI-SWS faculty member Derek Dreyer and his collaborators (including MPI-SWS alumni Ralf Jung, David Swasey, and Aaron Turon) have received the 2025 Most Influential POPL Paper Award for their POPL 2015 paper, "Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning" (https://iris-project.org/pdfs/2015-popl-iris1-final.pdf).  This comes on top of the Alonzo Church Award that they received in 2023 for the four core papers on the foundations of Iris.

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.

Award citation: This paper introduced Iris, a unifying framework for higher-order concurrent separation logic mechanized in the Rocq Prover (formerly Coq).  At the time Iris came along, the field of separation logic had become fractured, with many different and potentially incompatible logics being developed with bespoke models.  This first paper on Iris showed how a few key ingredients from prior work -- most notably, partial commutative monoids for representing user-defined ghost state (inspired by the Views framework) and higher-order impredicative invariants (inspired by step-indexed models) -- could be fruitfully combined to *derive* a wide variety of sophisticated proof techniques (such as “logically atomic triples”) that were built in as primitive in prior logics.  It was just the first step in a long line of work by a rich and diverse community of Iris developers from around the world.  Thanks to subsequent work on the Iris Proof Mode in Rocq, Iris has become a widely-used tool in both program verification and programming language meta-theory, with applications ranging from functional correctness proofs for low-level systems code (e.g. hypervisors, crash-safe systems, weak-memory data structures) to extensible semantic soundness proofs for high-level type systems (e.g. Rust, OCaml, Scala).

A video of the award presentation can be found here: https://www.youtube.com/live/ZKwpY0g9Lo8?si=scSr-qC9C44huJ_f&t=28949
Read more

Derek Dreyer becomes ACM Fellow

MPI-SWS scientific director Derek Dreyer was appointed as a Fellow by the Association for Computing Machinery (ACM), the largest computer science association in the world. Derek, who leads the “Foundations of Programming” research group, received this honor for his contributions to the logical and semantic foundations of programming languages.

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. ...
MPI-SWS scientific director Derek Dreyer was appointed as a Fellow by the Association for Computing Machinery (ACM), the largest computer science association in the world. Derek, who leads the “Foundations of Programming” research group, received this honor for his contributions to the logical and semantic foundations of programming languages.

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 55 new ACM Fellows were elected this year, thirteen of them in Europe and four in Germany.

Further Information: 
Read more

Max Planck researchers publish 9 papers at POPL 2025 + a new record!

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 9 papers accepted to POPL 2025.  This is the eighth year in a row that MPI-SWS researchers have published 5+ papers in POPL. Furthermore, as of this year, MPI-SWS faculty member Derek Dreyer has published 25 papers at POPL----a new record!

Congratulations to all our POPL authors! ...
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 9 papers accepted to POPL 2025.  This is the eighth year in a row that MPI-SWS researchers have published 5+ papers in POPL. Furthermore, as of this year, MPI-SWS faculty member Derek Dreyer has published 25 papers at POPL----a new record!

Congratulations to all our POPL authors!

  • Data Race Freedom à la Mode by Aina Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, Derek Dreyer   ***Recipient of a distinguished paper award.

  • A quantitative probabilistic relational Hoare logic by Martin Avanzini, Gilles Barthe, Benjamin Gregoire, Davide Davoli

  • Automating equational proofs in Dirac notation by Yingte Xu, Gilles Barthe, Li Zhou

  • Preservation of speculative constant-time by compilation by Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gregoire, Vincent Laporte

  • Sound and Complete Proof Rules for Probabilistic Termination by Rupak Majumdar, V.R. Sathiyanarayana

  • RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency by Pavel Golovin, Michalis Kokologiannakis, Viktor Vafeiadis

  • Model Checking C/C++ with Mixed-Size Accesses by Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis

  • Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning by Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan

  • Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
    Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, Taeyoung Yoon, Youngju Song, Chung-Kil Hur


 

 

 

 
Read more