Christina Giannoula will be joining the tenure-track faculty at our institute starting January 2026. She will lead the SPIN research group, and is actively seeking motivated students and researchers to join her team.

Christina's research interests lie at the intersection of computer architecture, computer systems, high-performance computing, and sustainable computing. Her current research focuses on the hardware/software co-design of emerging applications, particularly AI/ML, with modern computing systems. She designs solutions across the entire system stack, from software down to hardware—including algorithms, compilers, runtime systems, programming frameworks, and hardware engines—leveraging cutting-edge technologies such as processing-in-memory and memory disaggregation. Her work targets improvements in performance, scalability, programmability, and sustainability.

Prior to joining MPI-SWS, Christina was a Postdoctoral Researcher at the University of Toronto, where she received several research distinctions, including Postdoctoral Research Awards from the Vector Institute for Artificial Intelligence. She was selected as a 2024 MLSys Rising Star and 2024 EECS Rising Star. She received her Ph.D. from the School of Electrical and Computer Engineering (ECE) at the National Technical University of Athens (NTUA) in Greece, where she was a member of the Computing Systems Laboratory. Her Ph.D. thesis received the 2022 Iakovos Gurounian Award for the Ph.D. thesis with the highest industrial impact.

Mariya Toneva, head of the Bridging AI and Neuroscience group at MPI-SWS, has been awarded a 2025 ERC Starting Grant. Over the next five years, her project BrainAlign will receive funding of nearly 1.5 million euros for research on "brain-aligned language models for long-range language understanding and neuroscientific insight." Read more about the BrainAlign project below.

In addition, former MPI-SWS postdoctoral fellow Jiarui Gan, who is currently a lecturer at Oxford, has also received a 2025 ERC Starting Grant for his project "Algorithms of Stochastic Principal-Agent Coordination".

ERC grants are the most prestigious and the most competitive European-level awards for ground-breaking scientific investigations. This year, less than 13% of all ERC Starting Grant applicants across all scientific disciplines received the award, with only 24 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 the 2025 ERC Starting Grants here: https://erc.europa.eu/news-events/news/starting-grants-2025-call-results

The BrainAlign Project

The BrainAlign project aims to revolutionize next-generation artificial intelligence (AI) models by aligning them closely with the way the human brain understands language. While AI systems for language understanding and generation have undergone much progress in recent years thanks to language models, these systems still face significant challenges, such as understanding human intent. Moreover, the successes have mostly stemmed from tremendous increases in model size, and continuing this trend demands unrealistic amounts of data, compute power, and energy.

One way forward is to look to the only system we trust to truly understand complex language: the human brain. Insights from brain functions have long inspired AI, but these insights took years to consolidate and even longer to transfer to AI. For brain functions that are uniquely human, such as understanding complex natural language, the lack of a suitable animal model organisms limits the mechanistic insights that can be applied to AI.

The BrainAlign project presents a novel, data-driven solution that will develop brain-aligned language models by forcing their internal processing to closely reflect information sampled directly from the human brain, as humans read and listen to large amounts of every-day language. By integrating machine learning techniques with human neuroimaging and behavioral data from novel experimental paradigms, BrainAlign will develop next-generation models with a deeper, human-like understanding of language. Additionally, innovative interpretability methods will allow these models to serve as model organisms, revealing mechanisms that mirror human brain processing of language and massively enhancing our scientific knowledge of language in the brain.

 

As part of our periodic evolution and development, MPI-SWS is organizing an (in-person) symposium on research topics of emerging interest in the broad area of software systems. we have invited six top researchers from around the world to participate: Natacha Crooks (UC Berkeley), Alexandra Silva (Cornell University), Maria Christakis (TU Wien), Stefanie Jegelka (TU Munich), Zeynep Akata (Helmholtz Munich & TU Munich), and Elissa Redmiles (Georgetown University).

The MPI-SWS Research Symposium will take place at MPI-SWS on June 10 and 11: at the Saarbrücken site on June 10, and at the Kaiserslautern site on June 11.

The full schedule can be found here: https://research-symposium-2025.mpi-sws.org/

 

 

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.

 

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

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: 

• https://www.acm.org/media-center/2025/january/fellows-2024


• https://awards.acm.org/fellows/award-winners


• https://www.mpi-sws.org/people/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 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