Programming Languages & Verification

The group’s research focuses on the principles, design and implementation of programming languages and on foundational techniques and practical tools for analyzing, testing, and verifying programs against their correctness specifications.

Recent research has developed techniques for verifying compilers and other critical software, and tools for testing and/or verifying concurrent systems.

News

Rupak Majumdar awarded ERC Advanced Grant

June 2026

Rupak Majumdar has been awarded an ERC Advanced Grant worth approximately €2.5 million for his project „Pascal: Formal Performance Analysis at Scale“. The project aims to develop new mathematical foundations and practical tools for analyzing and verifying the performance and resilience of large-scale distributed computer systems.

Derek Dreyer receives 2026 SIGPLAN Distinguished Service Award

June 2026

MPI-SWS Director Derek Dreyer has been awarded the the ACM Special Interest Group on Programming Languages 2026 Distinguished Service Award.

MPI researchers receive Distinguished Paper Award at PLDI 2026

June 2026

MPI-SWS researchers have received a PLDI 2026 Distinguished Paper Award for their paper "VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System."

Derek Dreyer achieves a publication record!

February 2026

MPI-SWS faculty member Derek Dreyer has published a total of 61 papers across all four flagship SIGPLAN conference---a new record!

Most downloaded PACMPL paper of 2025

January 2026

The paper "Tree Borrows" was in the year 2025 the single most downloaded article from all issues of the entire PACMPL journal.

All News

Recent projects

Recent software

genmc

Generic model checker for concurrent C programs

POROUS

An invariant builder and reachability checker for affine programs.

Papers

A Recipe for Modular Verification of Generic Tree Traversals.

Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg.
CPP 2026.

Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures.

C. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schütze, Georg Zetzsche.
POPL 2026.

Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation.

Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler.
POPL 2026.

General Decidability Results for Systems with Continuous Counters.

A. R. Balasubramanian, Matthew Hague, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche.
POPL 2026.

Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.

Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya.
CONCUR 2025.

All papers

People

Faculty

Björn Brandenburg

Derek Dreyer

Deepak Garg

Rupak Majumdar

Joel Ouaknine

Anne-Kathrin Schmuck

Viktor Vafeiadis

Georg Zetzsche

Research Group Leaders

Sadegh Soudjani

Mikhail Starchak

Research Scientist

Rameez Khan

Affiliated Faculty

Robert Harper
(External Scientific Member)

Anthony Lin
(Max Planck Fellow)

Postdoctoral Researchers

Cookie	Duration	Description
cookielawinfo-checkbox-analytics	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Analytics".
cookielawinfo-checkbox-functional	11 months	The cookie is set by GDPR cookie consent to record the user consent for the cookies in the category "Functional".
cookielawinfo-checkbox-necessary	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookies is used to store the user consent for the cookies in the category "Necessary".
cookielawinfo-checkbox-others	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Other.
cookielawinfo-checkbox-performance	11 months	This cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Performance".
viewed_cookie_policy	11 months	The cookie is set by the GDPR Cookie Consent plugin and is used to store whether or not user has consented to the use of cookies. It does not store any personal data.

Need help?