The 2025 Salomaa prize has been awarded to MPI-SWS faculty member Georg Zetzsche "for the breadth and depth of his results in formal languages, automata theory, and logic, particularly the theory of downward closures, decidability in infinite-state systems, algorithmic group theory, and arithmetic theories, connecting formal languages and computation in the spirit of Arto Salomaa.”

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.

 

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