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

Joël Ouaknine receives LICS test-of-time award

June 2025

Joël Ouaknine has received the 2025 LICS test-of-time award for his 2005 paper on Metric Temporal Logic.

Derek Dreyer receives most influential POPL paper award

January 2025

MPI-SWS faculty member Derek Dreyer has been selected as the winner of this year's POPL (Principles of Programming Languages) Most Influential Paper Award…

Derek Dreyer becomes ACM Fellow

January 2025

Derek Dreyer was appointed as a Fellow by the Association for Computing Machinery, for his contributions to the logical and semantic foundations of programming languages.

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

January 2025

Max Planck researchers have authored nine papers to appear in POPL 2025.

Michael Sammler wins Runner-Up Prize for Informatics Europe Best Dissertation Award

November 2024

Dr. Michael Sammler has received the Runner-Up Prize for the 2024 Informatics Europe Best Dissertation Award, as well as the Dr. Eduard Martin Prize from Saarland University.

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

Analyzing Metastable Failures.

Rebecca Isaacs, Peter Alvaro, Rupak Majumdar, Kiran Kumar, Muniswamy Reddy, Mahmoud Salamati, Sadegh Soudjani.
HotOS 2025.

Integrated Task and Path Planning for Collaborative Multi-Robot Systems.

Aman Aryan, Manan Modi, Indranil Saha, Rupak Majumdar, Swarup Mohalik.
ICCPS 2025.

Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification.

Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar.
IEEE Trans. Software Eng. 2025.

On the Monniaux Problem in Abstract Interpretation.

Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, James Worrell.
J. ACM 2025.

Destabilizing Iris.

Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, Derek Dreyer.
OOPSLA1 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

Affiliated Faculty

Maria Christakis
(Adjunct Faculty)

Eva Darulova
(Adjunct Faculty)

Robert Harper
(External Scientific Member)

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?