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

Five MPI-SWS papers at POPL 2019!

January 2019

Just as in 2018, MPI-SWS researchers again authored a total of five POPL papers in 2019.

More

MPI-SWS researchers win OOPSLA 2018 Distinguished Paper award

December 2018

Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic have won a Distinguished Paper award at OOPSLA 2018.

More

Derek Dreyer wins OOPSLA 2018 Distinguished Reviewer Award

December 2018

Derek Dreyer was one of two PC members (out of 30) to win a Distinguished Reviewer Award at OOPSLA 2018.

More

Program Analysis course at TU Kaiserslautern and Saarland University

October 2018

Maria Christakis and Eva Darulova are teaching Program Analysis at TU Kaiserslautern and Saarland University.

More

OOPSLA'18: Four MPI-SWS papers

September 2018

In 2018, MPI-SWS members published four papers at the SPLASH/OOPSLA research track.

More

All News

Recent projects

Daisy

a framework for accuracy analysis and synthesis of numerical programs

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

All projects

Recent software

adiff

Tool for differentially testing soundness and precision of program analyzers

bran

Static analysis framework for EVM bytecode

daisy

A framework for analysis and optimization of numerical programs

genmc

Generic model checker for concurrent C programs

Papers

Cost-sensitive classifier chains: Selecting low-cost features in multi-label classification.

Pawel Teisseyre, Damien Zufferey, Marta Slomka.
Pattern Recognition 2019.

Bridging the gap between programming languages and hardware weak memory models.

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
POPL 2019.

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
POPL 2019.

From fine- to coarse-grained dynamic information flow control and back.

Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan.
POPL 2019.

Grounding thin-air reads with event structures.

Soham Chakraborty, Viktor Vafeiadis.
POPL 2019.

All papers

People

Faculty

Björn Brandenburg

Maria Christakis

Eva Darulova

Derek Dreyer

Deepak Garg

Rupak Majumdar

Joel Ouaknine

Viktor Vafeiadis

Georg Zetzsche

Research Group Leaders

Daniel Neider

Damien Zufferey

Postdoctoral Researchers

Engel Lefaucheux

Rodolphe Lepigre

Azalea Raad

Anne-Kathrin Schmuck

Burcu Özkan

Doctoral Students

Rosa Abbasi

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

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

Filip Niksic

Michael Rainey

Aaron Turon

Johar Ashfaque

Ventsislav Chonev

Ezgi Cicek

Rayna Dimitrova

Sadegh Esmaeil Zadeh Soudjani

Anastasiia Izycheva

Scott Kilpatrick

Johannes Kloos

Georg Neis

Marco Patrignani

Willard Rafnsson

Andreas Rossberg

Alexander Wieder

Mustafa Zengin

Vinayak Prabhu

Pierre-Marie Pédrot

Ruzica Piskac