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

POPLpalooza: Five MPI-SWS papers at POPL 2018 + a new record!

January 2018

In 2018, MPI-SWS researchers authored a total of five POPL papers. Also, MPI-SWS faculty member Derek Dreyer has achieved a new record: a 10-year streak of having at least one POPL paper each year.

More

Maria Christakis receives Facebook Faculty Research Award

December 2017

MPI-SWS faculty member Maria Chistakis has received a Facebook Faculty Research Award for her work on combining static and dynamic program analysis.

More

Two MPI-SWS faculty awarded DFG grants

December 2017

MPI-SWS faculty members Björn Brandenburg and Eva Darulova have each received a 3-year research grant from the DFG, the German Research Organization.

More

MPI-SWS researchers win OOPSLA 2017 Distinguished Paper award

October 2017

David Swasey, Deepak Garg, and Derek Dreyer have won a Distinguished Paper award at OOPSLA 2017.

More

MPI-SWS wins best-paper awards at PLDI and ECOOP

June 2017

MPI-SWS researchers won best-paper awards at PLDI 2017 and at ECOOP 2017.

More

All News

Recent projects

FSL

A program logic for C11 concurrency with support for memory fences

IRIS

A concurrent program logic based on monoids and invariants

RustBelt

Logical foundations for the future of safe systems programming

OGRA

The Owicki-Gries method for the RA memory model

GPS

A program logic for C11 concurrency

C11comp

Reasoning about C11 program transformations

All projects

Papers

PhD Thesis: Relational Cost Analysis

Ezgi Çiçek.
Technical Report MPI-SWS-2018-006 2018.

Reachability analysis of reversal-bounded automata on series-parallel graphs.

Rayna Dimitrova, Rupak Majumdar.
Acta Inf. 2018.

Effective stateless model checking for C/C++ concurrency.

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis.
POPL 2018.

Monadic refinements for relational cost analysis.

Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
POPL 2018.

Parametricity versus the universal type.

Dominique Devriese, Marco Patrignani, Frank Piessens.
POPL 2018.

All papers

People

Faculty

Björn Brandenburg

Maria Christakis

Eva Darulova

Derek Dreyer

Deepak Garg

Rupak Majumdar

Joel Ouaknine

Viktor Vafeiadis

Research Group Leaders

Daniel Neider

Damien Zufferey

Postdoctoral Researchers

Johar Ashfaque

Pierre-Marie Pédrot

Azalea Raad

Anne-Kathrin Schmuck

Burcu Özkan

Doctoral Students

Heiko Becker

Soham Chakraborty

Hoang-Hai Dang

Marko Doko

Akram El-Korashy

Ivan Gavran

Ralf Jung

Jan-Oliver Kaiser

Michalis Kokologiannakis

Debasmita Lohar

Kaushik Mallik

Muhammad Numair Mansur

Aman Shankar Mathur

Filip Niksic

Simin Oraee

Marcus Pirron

Vineet Rajani

Mahmoud Salamati

David Swasey

Joshua Yanovski

Former members

Matthew Hammer

Chung-Kil Hur

Jacques-Henri Jourdan

Neel Krishnaswami

Boris Köpf

Ori Lahav

Michael Rainey

Aaron Turon

Ventsislav Chonev

Ezgi Cicek

Rayna Dimitrova

Joshua Dunfield

Sadegh Esmaeil Zadeh Soudjani

Shahram Esmaeilsabzali

Marko Horvat

Anastasiia Izycheva

Scott Kilpatrick

Johannes Kloos

Adrian Leva

Georg Neis

Marco Patrignani

Willard Rafnsson

Andreas Rossberg

Samira Safaei Farahani

Alexander Wieder

Mustafa Zengin

Vinayak Prabhu

Umut Acar

Ruzica Piskac