News
Programming Languages & Verification
Derek Dreyer receives most influential POPL paper award
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. ...
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
Derek Dreyer becomes ACM Fellow

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. ...
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:
Max Planck researchers publish 9 papers at POPL 2025 + a new record!
Congratulations to all our POPL authors! ...
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
Michael Sammler wins Runner-Up Prize for Informatics Europe Best Dissertation Award

Michael's dissertation is entitled "Automated and Foundational Verification of Low-Level Programs", ...
Michael's dissertation is entitled "Automated and Foundational Verification of Low-Level Programs", and was supervised by MPI-SWS faculty Deepak Garg and Derek Dreyer.
Michael's dissertation has also received the Dr. Eduard Martin Prize from Saarland University.
Michael is currently doing a postdoc at ETH Zurich with Peter Müller, and in January 2025 he will start as a tenure-track faculty at IST Austria.
Congratulations, Michael, on this richly deserved honor!!!
MPI-SWS researchers receive SOSP'24 Distinguished Artifact Award

Traditional software testing methods will reveal bugs, but testing alone can’t guarantee the absence of errors. Software verification tools such as Verus mathematically prove that software behaves according to its specifications. ...
MPI-SWS researcher receives OSDI 2024 Best Paper Award
MPI-SWS researchers receive PLDI 2024 Distinguished Artifact Award
Max Planck researchers publish 7 papers at POPL 2024!
- Decision and Complexity of Dolev-Yao Hyperproperties by Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind
- Parikh's Theorem Made Symbolic by Matthew Hague,
- Decision and Complexity of Dolev-Yao Hyperproperties by Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind
- Parikh's Theorem Made Symbolic by Matthew Hague, Artur Jez, Anthony Widjaja Lin
- Positive Almost-Sure Termination – Complexity and Proof Rules by Rupak Majumdar and V.R. Sathiyanarayana.
- Ramsey Quantifiers in Linear Arithmetics by Pascal Bergsträßer, Moses Ganardi, Anthony Widjaja Lin, Georg Zetzsche
- Reachability in Continuous Pushdown VASS by A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
- Regular Abstractions for Array Systems by Chih-Duo Hong and Anthony Widjaja Lin
- Securing Verified IO Programs Against Unverified Code in F* by Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
MPI-SWS PhD students appointed as tenure-track faculty at ETH Zurich and ISTA
Michalis Kokologiannakis, a doctoral student in the Software Analysis and Verification group, has accepted a tenure-track faculty position at ETH Zurich. Michalis is broadly interested in programming languages, compilers, weak memory models, and software verification. More specifically, he is interested in developing novel algorithmic techniques for verifying concurrent software, ...
Michalis Kokologiannakis, a doctoral student in the Software Analysis and Verification group, has accepted a tenure-track faculty position at ETH Zurich. Michalis is broadly interested in programming languages, compilers, weak memory models, and software verification. More specifically, he is interested in developing novel algorithmic techniques for verifying concurrent software, while also taking into account the weak memory models employed by modern microprocessors. You can find out more about his work at https://people.mpi-sws.org/~michalis/.
Michael Sammler, a doctoral student in the Foundations of Computer Security and Foundations of Programming groups, has accepted a tenure-track faculty position at the Institute of Science and Technology Austria (ISTA). Before starting at ISTA, he will spend one year as a postdoctoral fellow in the Programming Methodology Group at ETH Zurich. Michael's research interests lie in implementing efficient and practical systems and formally proving properties about them. In particular, his research focuses on building formal verification tools for low-level systems code that combine foundational proofs in a proof assistant with a high degree of automation. You can find out more about his work at https://people.mpi-sws.org/~msammler/ and https://ista.ac.at/en/research/sammler-group/.
Congratulations Michael and Michalis!
MPI-SWS researchers receive the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation

- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon,
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer: “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning”. POPL 2015.
- Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ICFP 2016.
- Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. ESOP 2017.
- Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).
More details about the Alonzo Church Award and about the 2023 Church Award.
Kaushik Mallik awarded ETAPS Doctoral Dissertation Award
This is the second time that the ETAPS Doctoral Dissertation Award was given to an MPI-SWS student. In 2021 it was awarded to Ralf Jung for his thesis on Understanding and Evolving the Rust Programming Language, supervised by Derek Dreyer.
Max Planck researchers publish 6 papers at POPL 2023!
- Conditional Contextual Refinement by Youngju Song,
- Conditional Contextual Refinement by Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
- Context-Bounded Verification of Context-Free Specifications by Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
- DimSum: A Decentralized Approach to Multi-language Semantics and Verification by Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer. DISTINGUISHED PAPER
- Kater: Automating Weak Memory Model Metatheory and Consistency Checking by Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
- The Path to Durable Linearizability by Emanuele D’Osualdo, Azalea Raad, Viktor Vafeiadis
- CoqQ: Foundational Verification of Quantum Programs by Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
Ralf Jung accepts faculty position at ETH Zurich

Ralf's primary research interest is in developing formal foundations and tools that establish machine-checked guarantees for real-world software systems. To achieve this, his work spans all the way from foundational and deeply theoretical to applied, from proving theorems to developing tools used by other researchers and software developers.. ...
Ralf's primary research interest is in developing formal foundations and tools that establish machine-checked guarantees for real-world software systems. To achieve this, his work spans all the way from foundational and deeply theoretical to applied, from proving theorems to developing tools used by other researchers and software developers.. You can find out more about his work at https://research.ralfj.de/.
Simon Spies receives 2022 Google Fellowship

The Google PhD Fellowship Program was created to recognize outstanding graduate students doing exceptional and innovative research in areas relevant to computer science and related fields. Simon, who is advised by Derek Dreyer, was the only student in the area of Programming Technology and Software Engineering to receive a fellowship in 2022. ...
The Google PhD Fellowship Program was created to recognize outstanding graduate students doing exceptional and innovative research in areas relevant to computer science and related fields. Simon, who is advised by Derek Dreyer, was the only student in the area of Programming Technology and Software Engineering to receive a fellowship in 2022.
Link: https://research.google/outreach/phd-fellowship/
Derek Dreyer to chair POPL 2024
POPL is the premier venue in the area of programming languages and, alongside PLDI, ranks as one of the top two international conferences on this topic.
Principles of Programming Languages is the premier forum for the fundamental innovations in design, definition, analysis, ...
POPL is the premier venue in the area of programming languages and, alongside PLDI, ranks as one of the top two international conferences on this topic.
Principles of Programming Languages is the premier forum for the fundamental innovations in design, definition, analysis, transformation, and implementation of programming languages, programming systems, and programming abstractions.
Rupak Majumdar wins CONCUR test-of-time award
The award citation reads as follows: "The paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. ...
The award citation reads as follows: "The paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. A key contribution of the paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise as they are played "faster", and the definition of natural concepts of winning conditions for the two players -- ensuring that players can win only by playing according to a physically meaningful strategy. This approach provides a clean answer to the problem of time convergence, and the responsibility of the players in it. For this reason, it has since been the basis of numerous works on timed games. The algorithm established in the paper to study omega-regular conditions in this neat model of timed games is also enticing, resorting to mu-calculus on a cleverly enriched structure."
Viktor Vafeiadis receives Robin Milner Young Researcher Award

"Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep, ...
"Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep, the first extension of concurrent separation logic to support formal proofs about fine-grained concurrent algorithms. His work on Cave presented the first fully automatic verifier for establishing linearizability of a class of concurrent data structures, including ones with non-fixed linearization points. His work on CompCertTSO presented the first verified compiler for a concurrent language under a relaxed memory model. He developed the first direct (and mechanized) proof of soundness for concurrent separation logic (CSL) based on operational semantics—beautifully simple compared to prior proofs and a key enabler for proving soundness of more advanced program logics like CAP and Iris. He developed the first separation logic for the C/C++ relaxed memory model—a tour-de-force achievement compared to the standard CSL which assumes sequential consistency. This spawned a whole body of work on modular verification of concurrent data structures under relaxed memory models. His work has found and corrected a number of serious flaws in the C/C++ concurrency model, which led to changes in the C++ standard. And his "promising" semantics for relaxed-memory concurrency offered one of the first viable solutions to the 30-year-old "out-of-thin-air" problem and spawned much follow-on work. His work on GenMC presented the first efficient model checkers for relaxed-memory C/C++ programs with optimality guarantees about their state space exploration. Recent work together with his postdoc Azalea Raad (now faculty at Imperial), presented the first "persistency semantics" for non-volatile memory on multicore architectures. Viktor is not only highly-cited and incredibly prolific—he is also a true pioneer, repeatedly exploring dauntingly technical problems in the semantics and verification of concurrent programs before others dare to try."
This award makes MPI-SWS the only institution in the world to boast two recipients of the SIGPLAN Milner award among its faculty.
Two faculty win prestigious Google Research Scholar awards
Two MPI-SWS faculty, Maria Christakis and Elissa Redmiles, have earned highly competitive Google Research Scholar awards. Maria Christakis's award was given for her research on metamorphic specification and testing of machine-learning models and Elissa Redmiles's award was given for her research on aligning technical data privacy protections with user concerns.
The Google Research Scholar Program provides unrestricted gifts of up to $60,000 to support research at institutions around the world and is focused on funding world-class research conducted by early-career professors. ...
Two MPI-SWS faculty, Maria Christakis and Elissa Redmiles, have earned highly competitive Google Research Scholar awards. Maria Christakis's award was given for her research on metamorphic specification and testing of machine-learning models and Elissa Redmiles's award was given for her research on aligning technical data privacy protections with user concerns.
The Google Research Scholar Program provides unrestricted gifts of up to $60,000 to support research at institutions around the world and is focused on funding world-class research conducted by early-career professors. Award proposals go through an internal, merit-based review process and selected faculty can receive a Google Research Scholar award only once in their career. Award recipients are assigned a liaison at the company to share findings with and as a point of contact for further collaboration.
Derek Dreyer appointed MPI-SWS Director

Derek became known for his pioneering work in programming languages and verification, with a particular emphasis on building rigorous foundations for establishing the reliability and correctness of realistic software systems. In recent years, he and his group have become especially well known for their work on the Iris and RustBelt verification frameworks, ...
Derek became known for his pioneering work in programming languages and verification, with a particular emphasis on building rigorous foundations for establishing the reliability and correctness of realistic software systems. In recent years, he and his group have become especially well known for their work on the Iris and RustBelt verification frameworks, both implemented in the Coq proof assistant. Developed initially in 2015, Iris is a system for developing and deploying higher-order concurrent separation logics; though only 7 years old, it has already been used in over 60 papers published in top venues in programming languages. One of the most significant applications of Iris is RustBelt, which constitutes the first formal, machine-checked foundation for verifying the safety of the increasingly popular systems programming language Rust. These large-scale verification efforts place Dreyer's group at the forefront of programming languages research worldwide.
Derek has received numerous accolades for his research, teaching, and service, including the 2017 ACM SIGPLAN Robin Milner Young Researcher Award, a 2015 ERC Consolidator Grant, multiple Distinguished Paper Awards at top conferences like POPL, PLDI, and OOPSLA, the OOPSLA'18 Distinguished Reviewer Award, and most recently, the "Busy Beaver Award" at Saarland University for outstanding commitment to teaching. Under his mentorship, members of his group have also received numerous awards, including the prestigious ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award and ACM Doctoral Dissertation Honorable Mention Award (for Dr. Ralf Jung).
Derek was born in New York City in 1980. He holds a Bachelor's in Mathematics and Computer Science from New York University and received his PhD in Computer Science from Carnegie Mellon University in 2005. From 2005 to 2007, he was a Research Assistant Professor at the Toyota Technological Institute at Chicago. He joined MPI-SWS as a tenure-track faculty in January 2008, only a few years after the Institute's founding, and has been an integral member ever since. We are thus very proud to be able to retain him as a Scientific Director of the institute.
Joël Ouaknine appointed ACM Fellow

ACM has also elected as Fellows two researchers from our neighboring Max Planck Institute for Informatics: Thomas Lengauer is recognized for contributions to bioinformatics and medical informatics and Bernt Schiele is recognized for contributions to large-scale object recognition, ...
ACM has also elected as Fellows two researchers from our neighboring Max Planck Institute for Informatics: Thomas Lengauer is recognized for contributions to bioinformatics and medical informatics and Bernt Schiele is recognized for contributions to large-scale object recognition, human detection, and pose estimation.
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 71 new ACM Fellows were elected this year, twelve of them in Europe, four in Germany and three of them in Saarbrücken.
Further Information:
Bob Harper receives ACM SIGPLAN Achievement Award

Award Citation:
Robert (Bob) Harper is widely known for his foundational contributions to our understanding of type theory and its use in the design, ...
Award Citation:
Robert (Bob) Harper is widely known for his foundational contributions to our understanding of type theory and its use in the design, specification, implementation, and verification of modern programming languages. Bob demonstrated that sound type systems and operational semantics are not only appropriate vehicles for reasoning about idealized languages, but that this theory can be applied to complex, modern languages. His achievements include analysis of language features ranging from references to continuations to modules, the definition of a variety of new type systems, the idea of using types throughout the compilation process, the analysis of run-time system semantics and cost, a formal definition of Standard ML and its mechanization, the definition of logical framework LF and other logical frameworks based on homotopy type theory.
Some of Bob’s most influential work involved the design, theory and implementation of the TIL (Typed Intermediate Language) compiler system, which pioneered the idea that compilers can propagate type information to lower-level intermediate languages, where it can be used to guide optimizations and to catch compiler bugs. These ideas led directly to the development of proof-carrying code, typed assembly language, and a wide array of type-preserving compilers.
Bob Harper has also had a profound impact though his mentorship, teaching and the influence of his books “Programming in Standard ML” and “Practical Foundations for Programming Languages.”
Max Planck researchers publish 11 papers at POPL 2022!
- Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine,
- Concurrent Incorrectness Separation Logic Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn
- Context-Bounded Verification of Thread Pools Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
- Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal Stores Azalea Raad, Luc Maranget, Viktor Vafeiadis
- Isolation Without Taxation: Near Zero Cost Transitions for WebAssembly and SFI Matthew Kolosick, Shravan Ravi Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan
- Pirouette: Higher-Order Typed Functional Choreographies Andrew K. Hirsch, Deepak Garg. DISTINGUISHED PAPER
- Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer. DISTINGUISHED PAPER
- Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables Taolue Chen, Alejandro Flores Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Ruemmer, Zhilin Wu
- Subcubic Certificates for CFL Reachability Dmitry Chistikov, Rupak Majumdar, Philipp Schepper
- Truly Stateless, Optimal Dynamic Partial Order Reduction Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis
- VIP: Verifying Real-World C Idioms with Integer-Pointer Casts Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
- What's Decidable about Linear Loops? Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell
Sumit Gulwani awarded 2021 Max Planck Humboldt Medal

With a background in program analysis and artificial intelligence, Sumit Gulwani shaped the field of program synthesis, which emerged around 2010. The computer scientist developed algorithms that can efficiently generate computer programs from very few input-output examples, ...
With a background in program analysis and artificial intelligence, Sumit Gulwani shaped the field of program synthesis, which emerged around 2010. The computer scientist developed algorithms that can efficiently generate computer programs from very few input-output examples, natural-language-based specification, or from just the code and data context. His work made it possible for non-programmers to program tedious, repetitive spreadsheet tasks, and enabled productivity improvements for data scientists and developers for data wrangling and software engineering tasks. Recently, Sumit has also been using the tools of program synthesis for computer-aided education of pupils and students. Starting from the automatic correction of learners' work in programming education, he further evolved this line of work to detect misunderstandings and give learning feedback and grades, also in subjects like mathematics and language learning.
The medal comes with prize money in the amount of 60,000 euros.
MPI-SWS students receive ACM SIGPLAN Dissertation Award two years in a row
This is the second year in a row that the ACM SIGPLAN Dissertation Award was given to an MPI-SWS student. ...
This is the second year in a row that the ACM SIGPLAN Dissertation Award was given to an MPI-SWS student. Last year it was awarded to Filip Niksic for his thesis on Combinatorial Constructions for Effective Testing, supervised by Rupak Majumdar.
The award, first given in 2001, recognizes outstanding doctoral dissertations in the area of Programming Languages.
Ralf Jung receives ACM Doctoral Dissertation Award Honorable Mention

Ralf's work has previously received the ETAPS Doctoral Dissertation Award and the Otto Hahn Medal, as well as being featured in the April 2021 issue of Communications of the ACM in an article entitled "Safe Systems Programming in Rust". For more details see the Saarland Informatics Campus press release.
Otto Hahn Medal awarded to two MPI-SWS students

MPI-SWS researchers receive multiple awards at ETAPS
In addition, a TACAS 2021 paper by Rosa Abbasi and Eva Darulova (along with their collaborators Jonas Schiffl, Mattias Ulbrich, and Wolfgang Ahrendt) was one of only a handful of papers nominated for the EAPLS Best Paper Award: Deductive Verification of Floating-Point Java Programs in KeY. ...
ETAPS dissertation award and CACM article for Ralf Jung and his work on Rust

A committee of international experts evaluated candidate dissertations with respect to originality, ...
A committee of international experts evaluated candidate dissertations with respect to originality, relevance, and impact to the field, as well as the quality of writing. The committee found that Dr. Ralf Jung's dissertation is very well-written and makes several highly original contributions in the area of programming language semantics and verification. The committee was also particularly impressed by the dissertation for its technical depth, the quality and quantity of the associated published work, as well as its relevance and impact both in academia and industry.
Ralf's work on Rust was also featured in a recent Communications of the ACM article: Safe Systems Programming in Rust by Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. The article appeared in the April 2021 issue of CACM, together with a short video about this work produced by ACM.
Max Planck researchers publish 8 papers at POPL 2021!
MPI-SWS papers:
- A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis Vineet Rajani, Marco Gaboardi, Deepak Garg, Jan Hoffmann
- Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche DISTINGUISHED PAPER
- Deciding ω-Regular Properties on Linear Recurrence Sequences Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, James Worrell
- Giving Semantics to Program-Counter Labels via Secure Effects Andrew Hirsch, Ethan Cecchetti
- PerSeVerE: Persistency Semantics for Verification under Ext4 Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
- Transfinite Step-Indexing for Termination Simon Spies, Neel Krishnaswami, Derek Dreyer
MPI-SP papers:
- A Pre-Expectation Calculus for Probabilistic Sensitivity Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja DISTINGUISHED PAPER
- Deciding Accuracy of Differential Privacy Schemes Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan
Viktor Vafeiadis awarded ERC Consolidator Grant

One of the other recipients of an ERC Consolidator Grant this year is an MPI alumnus: Neel Krishnaswami was an MPI-SWS postdoc with Derek Dreyer, ...
One of the other recipients of an ERC Consolidator Grant this year is an MPI alumnus: Neel Krishnaswami was an MPI-SWS postdoc with Derek Dreyer, and he is currently a faculty member at Cambridge.
ERC grants are the most prestigious and the most competitive European-level awards for ground-breaking scientific investigations. This year, less than 14% of all ERC Consolidator Grant applicants across all scientific disciplines received the award, with only 15 awardees in Computer Science across all of Europe! The ERC Consolidator Grant offers funding for researchers with 7 to 12 years of experience after achieving a PhD. You can find more information about ERC Consolidator Grants awarded this year at https://erc.europa.eu/news/CoG-recipients-2020.
The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, across all research areas. Talented researchers from all over the world can receive funding for excellent research in Europe.
The PERSIST Project
Non-volatile memory (NVM) is an emerging technology that provides orders of magnitude faster access to persistent storage (which preserves its contents after a crash or a power failure) than hard disks. As such, it is expected to radically change how modern applications manage storage, moving away from traditional block-structured file systems to in-memory persistent data structures.
The problem with NVM, however, is that its programming model is standing on very shaky foundations. The persistency semantics of the mainstream architectures is unclear and full of counterintuitive behaviours, which makes writing correct NVM programs a very challenging task.
The project's goal is to develop a solid mathematical basis for determining the semantics of NVM programs and for reasoning about their correctness. More specifically, the plan is to produce:
- Formal persistency models for mainstream hardware architectures,
- Formal persistency models for mainstream programming languages,
- Firmly-grounded higher-level abstractions to ease persistent programming, and
- Effective testing and verification techniques for persistent programs (e.g., program logics and model checking).
Filip Niksic awarded ACM SIGPLAN John C. Reynolds Dissertation Award
The award citation reads as follows: Soundness is at the core of most programming language verification techniques. On the other hand, random testing is one of the most commonly used techniques for analyzing software. ...
The award citation reads as follows: Soundness is at the core of most programming language verification techniques. On the other hand, random testing is one of the most commonly used techniques for analyzing software. Developing a theory of soundness for random testing is therefore a very important goal, but very few results existed before this thesis.Randomized techniques are seldom used in (sound) program analyses, which means that addressing the problem required the development of new ways to approaching it. Filip Niksic's thesis is among the first to apply deep techniques from randomized algorithms and combinatorics to the problem of understanding and explaining the effectiveness of random testing. Moreover, the theory helps with the design of new random testing approaches. The thesis addresses a hard problem, brining in novel theory from outside programming languages, and proving hard theorems. As scientists, when we see a phenomenon that we cannot immediately explain (in this case, the effectiveness of random testing), we should try to build a scientific explanation. For some problems, including random testing, it is unclear that one can actually formulate a precise theory, because the "real world" is extremely messy. The fact that Filip Niksic is able to formulate such problems precisely and prove nontrivial theorems about them is surprising and opens the door to a new field.
Anne-Kathrin Schmuck receives Emmy Noether Award
Anne-Kathrin's group will be hosted at MPI-SWS in Kaiserslautern and will develop automated modular synthesis techniques for reliable Cyber-Physical System (CPS) design. ...
Anne-Kathrin's group will be hosted at MPI-SWS in Kaiserslautern and will develop automated modular synthesis techniques for reliable Cyber-Physical System (CPS) design. Her work draws inspiration from both Control Theory and Computer Science and centers around Reactive Synthesis, Supervisory Control Theory and Abstraction-Based Controller Design.
Michael Sammler receives Google Fellowship

Link: https://research.google/outreach/phd-fellowship/
Max Planck researchers publish 17 papers at LICS/ICALP 2020
MPI-SWS papers:
- Invariants for Continuous Linear Dynamical Systems. Shaull Almagor, Edon Kelmendi, Joël Ouaknine and James Worrell. ICALP 2020, Track B. [ Video | Paper]
- The complexity of bounded context switching with dynamic thread creation. Pascal Baumann, Rupak Majumdar, Ramanathan Thinniyam Srinivasan and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]
- Extensions of ω-Regular Languages. Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański and Georg Zetzsche. LICS 2020. [ Video | Paper ]
- Rational subsets of Baumslag-Solitar groups. Michaël Cadilhac, Dmitry Chistikov and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]
- On polynomial recursive sequences. Michaël Cadilhac, Filip Mazowiecki, Charles Paperman, Michał Pilipczuk and Géraud Sénizergues. ICALP 2020, Track B. [ Video | Paper ]
- An Approach to Regular Separability in Vector Addition Systems. Wojciech Czerwiński and Georg Zetzsche. LICS 2020. [ Video | Paper ]
- The complexity of knapsack problems in wreath products. Michael Figelius, Moses Ganardi, Markus Lohrey and Georg Zetzsche. ICALP 2020, Track B. [ Video | Paper ]
- The Complexity of Verifying Loop-free Programs as Differentially Private. Marco Gaboardi, Kobbi Nissim and David Purser. ICALP 2020, Track B. [ Video | Paper ]
- On Decidability of Time-bounded Reachability in CTMDPs. Rupak Majumdar, Mahmoud Salamati and Sadegh Soudjani. ICALP 2020, Track B. [ Video | Paper ]
MPI-INF papers:
- Scheduling Lower Bounds via AND Subset Sum. Amir Abboud, Karl Bringmann, Danny Hermelin and Dvir Shabtay. ICALP 2020, Track A. [ Video | Paper ]
- Faster Minimization of Tardy Processing Time on a Single Machine. Karl Bringmann, Nick Fischer, Danny Hermelin, Dvir Shabtay and Philip Wellnitz. ICALP 2020, Track A. [ Video | Paper ]
- Hitting Long Directed Cycles is Fixed-Parameter Tractable. Alexander Göke, Dániel Marx and Matthias Mnich. ICALP 2020, Track A. [ Video | Paper ]
- A (2 + ε)-Factor Approximation Algorithm for Split Vertex Deletion. Daniel Lokshtanov, Pranabendu Misra, Fahad Panolan, Geevarghese Philip and Saket Saurabh. ICALP 2020, Track A. [ Video | Paper ]
- Hypergraph Isomorphism for Groups with Restricted Composition Factors. Daniel Neuen. ICALP 2020, Track A. [ Video | Paper ]
- Deterministic Sparse Fourier Transform with an l∞ Guarante. Yi Li and Vasileios Nakos. ICALP 2020, Track A. [ Video | Paper ]
MPI-SP papers:
- Deciding Differential Privacy for Programs with Finite Inputs and Outputs. Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla and Mahesh Viswanathan. LICS 2020. [ Video | Paper ]
- Universal equivalence and majority on probabilistic programs over finite fields. Charlie Jacomme, Steve Kremer and Gilles Barthe. LICS 2020. [ Video | Paper ]
Research Spotlight: Software Engineering for Machine Learning

In the Practical Formal Methods group at MPI-SWS, we have recently focused on applying techniques from Software Engineering, including static analysis and test generation, to validate and verify properties of neural networks, such as robustness and fairness. In the following, we give a brief overview of three research directions we have been pursuing in this setting.
Blackbox Fuzzing of Neural Networks
By now, it is well known that even very subtle perturbations of a correctly classified image, such as a street sign, could cause a neural network to classify the new image differently. Such perturbed images are referred to as adversarial inputs and pose a critical threat to important applications of Machine Learning, like autonomous driving.
In our group, we recently developed DeepSearch [1], a blackbox-fuzzing technique that generates adversarial inputs for image-classification neural networks. Starting from a correctly classified image, DeepSearch strategically mutates its pixels such that the resulting image is more likely to be adversarial. By using spatial regularities of images, DeepSearch is able to generate adversarial inputs, while only querying the neural network very few times, which entails increased performance of our technique. Moreover, through a refinement step, DeepSearch further reduces the already subtle pixel perturbations of an adversarial input.
Adversarial-Input Detection for Neural Networks
To protect neural networks against adversarial inputs, we have developed RAID [2], a runtime-monitoring technique for detecting whether an input to a neural network is adversarial. Our technique consists of training a secondary classifier to identify differences in neuron activation values between correctly classified and adversarial inputs. RAID is effective in detecting adversarial inputs across a wide range of adversaries even when it is completely unaware of the type of adversary. In addition, we show that there is a simple extension to RAID that allows it to detect adversarial inputs even when these are generated by an adversary that has access to our detection mechanism.
Fairness Certification of Neural Networks
Several studies have recently raised concerns about the fairness of neural networks. To list a few examples, commercial recidivism-risk and health-care systems have been found to be racially biased. There is also empirical evidence of gender bias in image searches, for instance when searching for “CEO”. And facial-recognition systems, which are increasingly used in law enforcement, have been found biased with respect to both gender and race. Consequently, it is critical that we design tools and techniques for certifying fairness of neural networks or characterizing their bias.
We make an important step toward meeting these needs by designing the LIBRA static-analysis framework [3] for certifying causal fairness of neural networks used for classification of tabular data. In particular, given input features considered sensitive to bias, a neural network is causally fair if its output classification is not affected by different values of the sensitive features. On a high level, our approach combines a forward and a backward static analysis. The forward pass aims to divide the input space into independent partitions such that the backward pass is able to effectively determine fairness of each partition. For the partitions where certification succeeds, LIBRA provides definite (in contrast to probabilistic) fairness guarantees; otherwise, it describes the input space for which bias occurs. We have designed this approach to be sound and configurable with respect to scalability and precision, thus enabling pay-as-you-go fairness certification.
References
[1] Fuyuan Zhang, Sankalan Pal Chowdhury and Maria Christakis. DeepSearch: Simple and Effective Blackbox Fuzzing of Deep Neural Networks. CoRR abs/1910.06296, 2019.
[2] Hasan Ferit Eniser, Maria Christakis and Valentin Wüstholz. RAID: Randomized Adversarial-Input Detection for Neural Networks. CoRR abs/2002.02776, 2020.
[3] Caterina Urban, Maria Christakis, Valentin Wüstholz and Fuyuan Zhang. Perfectly Parallel Fairness Certification of Neural Networks. CoRR abs/1912.02499, 2019.
Azalea Raad accepts faculty position at Imperial College London
Azalea's research is in the area of programming languages and verification, spanning several topics including non-volatile memory, persistency semantics, weak memory models, stateless model checking and program logics. You can read more about her work here.
Research Spotlight: Logic and Learning

In our research, we address these problems and develop intelligent tools that help engineers to build safe and reliable hardware, ...
In our research, we address these problems and develop intelligent tools that help engineers to build safe and reliable hardware, software, and cyber-physical systems. To this end, we employ a unique and promising strategy, which has recently also regained major attention in the artificial intelligence community: combining inductive techniques from the area of machine learning and deductive techniques from the area of mathematical logic (e.g., see the recent Dagstuhl seminar on "Logic and Learning", which was co-organized by one of our group members). Specifically, our research revolves around three topics, to which the remainder of this article is devoted: verification, synthesis, and formal specification languages.
Verification
Verification is an umbrella term referring to tools and techniques that formally prove that a given system satisfies its specification. In the context of software, a popular approach is deductive verification. The idea is easy to describe: first, the given program is augmented with annotations (typically loop invariants, pre-/post-conditions of method calls, and shape properties of data structures), which capture the developer's intent and facilitate the deductive reasoning in a later step; second, the program, together with its annotations, is translated into formulas in a suitable logic, called verification conditions; third, the verification conditions are checked for validity using automated theorem provers. Thanks to brilliant computer scientists, such as Edsger Dijkstra and Tony Hoare, as well as recent advances in constraint solving, the latter two steps can be (almost) entirely automated. However, the first step still remains a manual, error-prone task that requires significant training, experience, and ingenuity. In fact, this is one of the main obstacles preventing a widespread adaptation of formal verification in practice.
To also automate the challenging first step, we have developed a novel approach, called ICE learning [1], which intertwines inductive and deductive reasoning. The key idea is to pit a (deductive) program verifier against an (inductive) learning algorithm, whose goal is to infer suitable annotations from test-runs of the program and failed verification attempts. The actual learning proceeds in rounds. In each round, the learning algorithm proposes candidate annotations based on the data it has gathered so far. The program verifier then tries to prove the program correct using the proposed annotations. If the verification fails, the verifier reports data back to the learning algorithm explaining why the verification has failed. Based on this new information, the learning algorithm refines its conjecture and proceeds to the next round. The loop stops once the annotations are sufficient to prove the program correct.
ICE learning has proven to be a very powerful approach that allows fully automatic verification of a wide variety of programs, ranging from recursive and concurrent programs over numeric data types [1], to algorithms manipulating dynamically allocated data structures [2], to industry-size GPU kernels [3]. In addition, the principles underlying ICE learning can be lifted to other challenging verification tasks, such as the verification of parameterized systems [4] as well as—in ongoing research—to the verification of cyber-physical and AI-based systems. You might want to try a demo immediately in your browser.
Synthesis
Synthesis goes beyond verification and could be considered the holy grail of computer science. In contrast to checking whether a hand-crafted program meets its specification, the dream is to fully automatically generate software (or a circuit for that matter) from specifications in a correct-by-construction manner.
Although this dream is unrealistic in its whole generality, there exist various application domains in which automated synthesis techniques have been applied with great success. In our own research, for instance, we have developed techniques for synthesizing safety controllers for reactive, cyber-physical systems that have to interact with a complex–and perhaps only partially known–environment [5, 6]. Moreover, we have proposed a general framework for generating loop-free code from input-output examples and specifications written in first-order logic [7]. Similar to ICE learning, these methods combine inductive and deductive reasoning, thereby unveiling and exploiting synergies of modern machine learning algorithms and highly-optimized symbolic reasoning engines.
Formal Specification Languages
Both verification and synthesis rely on the ability to write correct formal specifications, which have to precisely capture the engineer’s intuitive understanding of the system in question. In practice, however, formalizing the requirements of a system is notoriously difficult, and it is well known that the use of standard formalisms such as temporal logics requires a level of sophistication that many users might never develop.
We have recently started a new research project to combat this serious obstacle. Its main objective is to design algorithms that learn formal specifications in interaction with human engineers. As a first step towards this goal, we have developed a learning algorithm for the specification language “Linear Temporal Logic (LTL)”, which is the de facto standard in many verification and synthesis applications. You might think of this algorithm as a recommender system for formal specifications: the human engineer provides examples of the desired and undesired behavior of the system in question, while the recommender generates a series of LTL specifications that are consistent with the given examples; the engineer can then either chose one of the generated specifications or provide additional examples and rerun the recommender.
In ongoing research, we are extending our learning algorithm to a wide range of other specification languages, including Computational Tree Logic, Signal Temporal Logic, and the Property Specification Language. Moreover, we are developing feedback mechanisms that allow for a tighter integration of the human engineer into the loop. Again, you can try our technology immediately in your browser.
References
[1] D’Souza, Deepak; Ezudheen, P.; Garg, Pranav; Madhusudan, P.; Neider, Daniel: Horn-ICE Learning for Synthesizing Invariants and Contracts. In: Proceedings of the ACM on Programming Languages (PACMPL), volume 2 issue OOPSLA, pages 131:1–131:25. ACM, 2018.
[2] Neider, Daniel; Madhusudan, P.; Garg, Pranav; Saha, Shambwaditya; Park, Daejun: Invariant Synthesis for Incomplete Verification Engines. In: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), volume 10805 of Lecture Notes in Computer Science, pages 232–250. Springer, 2018
[3] Neider, Daniel; Saha, Shambwaditya; Garg, Pranav; Madhusudan, P.: Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants. In: 26th International Static Analysis Symposium (SAS 2019), volume 11822 of Lecture Notes in Computer Science, pages 323–346. Springer, 2019
[4] Neider, Daniel; Jansen, Nils: Regular Model Checking Using Solver Technologies and Automata Learning. In: 5th International NASA Formal Method Symposium (NFM 2013), volume 7871 of Lecture Notes in Computer Science, pages 16–31. Springer, 2013
[5] Neider, Daniel; Topcu, Ufuk: An Automaton Learning Approach to Solving Safety Games over Infinite Graphs. In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of Lecture Notes in Computer Science, pages 204–221. Springer, 2016
[6] Neider, Daniel; Markgraf, Oliver: Learning-based Synthesis of Safety Controllers. In: 2019 International Conference on Formal Methods in Computer Aided Design (FMCAD 2019), pages 120–128. IEEE, 2019
[7] Neider, Daniel; Saha, Shambwaditya; Madhusudan, P.: Synthesizing Piece-wise Functions by Learning Classifiers. In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of Lecture Notes in Computer Science, pages 186–203. Springer, 2016
[8] Neider, Daniel; Gavran, Ivan: Learning Linear Temporal Properties. In: 2018 International Conference on Formal Methods in Computer Aided Design (FMCAD 2018), pages 148–157. IEEE, 2018
MPI-SWS student receives best presentation award at the iFM'19 PhD Symposium

Max Planck researchers publish 8 papers at POPL 2020 + a new record!
MPI-SWS papers:
- The Future is Ours: Prophecy Variables in Separation Logic. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs. [pdf]
- The High-Level Benefits of Low-Level Sandboxing. Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak. [pdf]
- Persistency Semantics of the Intel-x86 Architecture. Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis. [pdf]
- RustBelt Meets Relaxed Memory. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. [pdf]
- Stacked Borrows: An Aliasing Model for Rust. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. [pdf]
MPI-SP papers:
- Formal Verification of a Constant-Time Preserving C Compiler. Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu. [pdf]
- A Probabilistic Separation Logic. Gilles Barthe, Justin Hsu, Kevin Liao. [pdf]
- Relational Proofs for Quantum Programs. Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou. [pdf]
Former MPI-SWS postdoc receives ERC starting grant
Advanced Automata Theory Course at TU Kaiserslautern
Azalea Raad selected to attend Heidelberg Laureate Forum
The Heidelberg Laureate Forum gives young computer science and math researchers the opportunity to interact with some of the world's top scientists. The speakers for the 2019 Forum, for example, include 17 different Turing Award winners, ...
The Heidelberg Laureate Forum gives young computer science and math researchers the opportunity to interact with some of the world's top scientists. The speakers for the 2019 Forum, for example, include 17 different Turing Award winners, as well as numerous winners of the Fields Medal, the Abel Prize, and the ACM Prize in Computing.
Derek Dreyer general chair of ICFP'19
MPI-SWS researchers have a distinguished paper at POPL 2019
Five MPI-SWS papers at POPL 2019!
- Bridging the Gap Between Programming Languages and Hardware Weak Memory Models by Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis.
- From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan.
- Formal verification of higher-order probabilistic programs by Tetsuya Sato,
- Bridging the Gap Between Programming Languages and Hardware Weak Memory Models by Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis.
- From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan.
- Formal verification of higher-order probabilistic programs by Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
- Grounding Thin-Air Reads with Event Structures by Soham Chakraborty and Viktor Vafeiadis.
- On Library Correctness under Weak Memory Consistency by Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis.
What's more, the MPI-SWS Software Analysis and Verification group has a whole session to itself at POPL 2019. The weak memory session on Thursday, Jan 17, is comprised of the three papers by Viktor Vafeiadis, his students, postdocs, and collaborators.
MPI-SWS researchers receive OOPSLA 2018 Distinguished Paper award
Distinguished Paper awards are given to about 10% of papers at OOPSLA.
Derek Dreyer receive OOPSLA 2018 Distinguished Reviewer Award
Program Analysis course at TU Kaiserslautern and Saarland University
OOPSLA'18: Four MPI-SWS papers
- Horn-ICE Learning for Synthesizing Invariants and Contracts. Deepak D'Souza, Ezudheen P, Pranav Garg, Daniel Neider, P. Madhusudan.
- Randomized Testing of Distributed Systems with Probabilistic Guarantees. Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
- Reconciling High-level Optimizations and Low-level Code in LLVM.
- Horn-ICE Learning for Synthesizing Invariants and Contracts. Deepak D'Souza, Ezudheen P, Pranav Garg, Daniel Neider, P. Madhusudan.
- Randomized Testing of Distributed Systems with Probabilistic Guarantees. Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher.
- Reconciling High-level Optimizations and Low-level Code in LLVM. Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes.
- Persistence Semantics for Weak Memory. Azalea Raad, Viktor Vafeiadis.
Several Open Positions in the ERC-funded RustBelt Project
POSTDOCS: We are seeking exceptional candidates with a strong, internationally competitive track record of research in programming languages and/or verification. The primary criterion is quality, but I am particularly interested in candidates who have specialized expertise in one or more of the following areas:
- Rust
- substructural/ownership type systems
- verification of concurrent programs
- weak/relaxed memory models
- interactive theorem proving in Coq
- compiler verification
Experience programming in Rust is a welcome bonus, ...
POSTDOCS: We are seeking exceptional candidates with a strong, internationally competitive track record of research in programming languages and/or verification. The primary criterion is quality, but I am particularly interested in candidates who have specialized expertise in one or more of the following areas:
- Rust
- substructural/ownership type systems
- verification of concurrent programs
- weak/relaxed memory models
- interactive theorem proving in Coq
- compiler verification
Experience programming in Rust is a welcome bonus, but not required.
STUDENTS: We are seeking exceptional candidates who have at least some background in programming language theory and/or formal methods, and who are eager to work on deep foundational problems with the potential for direct impact on a real, actively developed language. A bachelor's or master's degree is required. For more details about the MPI-SWS graduate program, see here: https://www.mpi-sws.org/graduate-studies/.
Successful applicants will join the Foundations of Programming group, led by Derek Dreyer at the Max Planck Institute for Software Systems (MPI-SWS)
in Saarbruecken, Germany. Current and former postdocs in the group have included Andreas Rossberg (co-designer of WebAssembly), Chung-Kil Hur, Neel Krishnaswami, Aaron Turon (manager of the Rust project at Mozilla), Jacques-Henri Jourdan, Ori Lahav, Pierre-Marie Pédrot, and Azalea Raad. Current and former PhD students in the group have included Georg Neis, Beta Ziliani, Scott Kilpatrick, David Swasey, Ralf Jung, Jan-Oliver Kaiser, Hoang-Hai Dang, Marko Doko, and @pythonesque. The RustBelt project benefits from longstanding active collaborations with Viktor Vafeiadis (MPI-SWS), Lars Birkedal (Aarhus University), Chung-Kil Hur & Jeehoon Kang (Seoul National University), Deepak Garg (MPI-SWS), and Robbert Krebbers (TU Delft), as well as the many contributors to the Iris project (http://iris-project.org).
The working language at MPI-SWS is English.
Application deadline: OCTOBER 31. If you are interested in joining the RustBelt team and want to learn more about the project, please contact Derek Dreyer directly at dreyer@mpi-sws.org. To apply for a postdoc (or PhD student) position, please submit a CV (and/or grade transcript), research statement (or statement of purpose), and list of references to https://apply.mpi-sws.org.
For further information, see the project web page at: http://plv.mpi-sws.org/rustbelt/

POPLpalooza: Five MPI-SWS papers at POPL 2018 + a new record!
- Parametricity versus the Universal Type. Dominique Devriese, Marco Patrignani, Frank Piessens.
- Effective Stateless Model Checking for C/C++ Concurrency. Michalis Kokologiannakis, Ori Lahav, Kostis Sagonas, Viktor Vafeiadis.
- Monadic refinements for relational cost analysis. Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
- Why is Random Testing Effective for Partition Tolerance Bugs? Rupak Majumdar,
- Parametricity versus the Universal Type. Dominique Devriese, Marco Patrignani, Frank Piessens.
- Effective Stateless Model Checking for C/C++ Concurrency. Michalis Kokologiannakis, Ori Lahav, Kostis Sagonas, Viktor Vafeiadis.
- Monadic refinements for relational cost analysis. Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger.
- Why is Random Testing Effective for Partition Tolerance Bugs? Rupak Majumdar, Filip Niksic.
- RustBelt: Securing the Foundations of the Rust Programming Language. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer.
Furthermore, with the "RustBelt" paper, MPI-SWS faculty member Derek Dreyer cements a 10-year streak of having at least one POPL paper each year, breaking the all-time record of 9 years previously held by John Mitchell at Stanford. Congratulations Derek!
Maria Christakis receives Facebook Faculty Research Award
Two MPI-SWS faculty awarded DFG grants
Eva Darulova has received a single-PI DFG grant entitled "Automated Rigorous Verification and Synthesis of Approximations."
Björn Brandenburg has received a DFG grant entitled "RT-Proofs: Formal proofs for real-time systems." This award is for a collaborative grant, with co-PIs at INRIA (Grenoble), Verimag (Grenoble), ONERA (Toulouse), and TU Braunschweig (Germany).
Both projects are actively recruiting doctoral students. ...
Eva Darulova has received a single-PI DFG grant entitled "Automated Rigorous Verification and Synthesis of Approximations."
Björn Brandenburg has received a DFG grant entitled "RT-Proofs: Formal proofs for real-time systems." This award is for a collaborative grant, with co-PIs at INRIA (Grenoble), Verimag (Grenoble), ONERA (Toulouse), and TU Braunschweig (Germany).
Both projects are actively recruiting doctoral students. Interested students can apply online.
Automated Rigorous Verification and Synthesis of Approximations
Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus, when implementing real-world systems, approximations are inevitable, as are the errors introduced by them. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory, energy or runtime, effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff, we need to ensure that the computed results are sufficiently accurate, otherwise we risk disastrously incorrect results or system failures. Unfortunately, the current way of programming with approximations is mostly manual, and consequently costly, error prone and often produces suboptimal results.
The goal of this project is to develop an end-to-end system which approximates numerical programs in an automated and trustworthy fashion. The programmer will be able to write exact high-level code and our `approximating compiler' will generate an efficient implementation satisfying a given accuracy specification. In order to achieve this vision, we will develop novel sound techniques for verifying the accuracy of approximate numerical programs, as well as new synthesis approaches to generate such approximations automatically.
RT-Proofs: Formal proofs for real-time systems
Real-time systems, i.e., computer systems subject to stringent timing constraints, are at the heart of most modern safety-critical technologies, including automotive systems, avionics, robotics, and factory automation, to name just a few prominent domains in which incorrect timing can have potentially catastrophic consequences. To assure the always-correct operation of such systems, i.e., to make sure that they always react in a timely fashion even in a worst-case scenario, rigorous validation efforts are required prior to deployment. However, establishing that all timing constraints are met is far from trivial --- and requires sophisticated analysis techniques --- because software timing varies in complex and difficult to predict ways, e.g., due to scheduling delays, shared resources, or communication, even when executing on a dedicated processor. Unfortunately, the theoretical foundations of current analysis methods are not nearly as rock-solid as one might expect.
The key problem is that the state-of-the-art methods are backed by only informal or abbreviated proofs, which are typically difficult to understand, check, adapt, or reuse. As a result, there is a non-trivial risk of subtle, but fatal mistakes, either lingering in the published literature, or arising when combining results with unstated, inconsistent assumptions. And indeed, this is not just a hypothetical concern --- most famously, the timing analysis of the CAN real-time bus (widely deployed in virtually all modern cars) was refuted in 2007, 13 years after initial publication. Similarly, other lesser-known examples of incorrect worst-case analyses abound in the literature, including off-by-one errors, incorrect generalizations, and even claims that are simply wrong. Worse, even if the underlying theory is indeed flawless, there is still no guarantee that it is actually implemented correctly in the toolchains used in practice. In short, the state of the art in the analysis of safety-critical real-time systems leaves a lot to be desired --- informal "pen and paper" proofs are simply inadequate.
There is a better way: timing analysis results should be formally proved, machine-checkable, and independently verifiable. To this end, the RT-proofs project will lay the foundations for the computer-assisted verification of schedulability analysis results by (i) formalizing foundational real-time concepts using the Coq proof assistant and (ii) mechanizing proofs of busy-window-based end-to-end latency analysis, the analysis approach of greatest practical relevance (e.g., used by SymTA/S). Additionally, we will (iii) demonstrate with a practical prototype how trust in a vendor's toolchain can be established by certifying the produced analysis results (rather than the tool itself). Leading by example, RT-proofs will fundamentally raise the level of rigor, to the benefit of the academic community, tool vendors, and real-time systems engineers in practice.
MPI-SWS researchers win OOPSLA 2017 Distinguished Paper award
Distinguished Paper awards are given to about 10% of papers at OOPSLA.
Derek Dreyer receives Robin Milner Young Researcher Award

"Derek Dreyer has made deep, creative research contributions of great breadth. His areas of impact are as diverse as module systems, data abstraction in higher-order languages, mechanized proof systems and techniques, and concurrency models and semantics. ...
"Derek Dreyer has made deep, creative research contributions of great breadth. His areas of impact are as diverse as module systems, data abstraction in higher-order languages, mechanized proof systems and techniques, and concurrency models and semantics. He has refactored and generalized the complex module systems of SML and OCaml; devised logical relations and techniques that enabled advances in reasoning about higher-order imperative programs; and developed novel separation logics for modular verification of low-level concurrent programs. His research papers are a model of clarity and depth, and he has worked actively to translate his foundational ideas into practice – most recently with the RustBelt project to provide formal foundations for the Rust language. Additionally, Dreyer has contributed leadership, support, and mentorship in activities such as the PLMW series of workshops, which are instrumental in growing the next generation of PL researchers."
Previous recipients of the award have included Stephanie Weirich, David Walker, Sumit Gulwani, Lars Birkedal, and Shriram Krishnamurthi.
MPI-SWS researchers receive best-paper awards at PLDI and ECOOP
PLDI 2017: Repairing Sequential Consistency in C/C++11, by Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer.
ECOOP 2017: Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris, by Jan-Oliver Kaiser, ...
PLDI 2017: Repairing Sequential Consistency in C/C++11, by Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer.
ECOOP 2017: Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris, by Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis.
In addition, another PLDI best paper award went to the paper "Bringing the Web Up to Speed with WebAssembly", which was presented by Andreas Rossberg, former member of the Foundations of Programming group, who is now a senior engineer at Google. WebAssembly is the result of an unprecedented collaboration between engineers at Google, Microsoft, Mozilla, and Apple to develop a new portable low-level byte code language to replace JavaScript as a target language for web development.
Maria Christakis to join MPI-SWS as tenure-track faculty

Maria joins MPI-SWS from the University of Kent, England, where she is a Lecturer at the School of Computing. She was previously a postdoctoral researcher at Microsoft Research Redmond. Maria received her Ph.D. from the Department of Computer Science of ETH Zurich and was awarded with the ETH medal and the EAPLS Best PhD Dissertation Award. She completed her Bachelor’s and Master’s degrees at the Department of Electrical and Computer Engineering of the National Technical University of Athens, Greece.
Static Program Analysis Course at Saarland University
Principles of Cyber-Physical Systems Course at TU Kaiserslautern
The course meets Tuesdays 11:45-13:15 and Thursdays 10:00-11:30 in 11-260.
Advanced Automata Theory Course at TU Kaiserslautern
The course meets Tuesdays 08:15-09:45 in room 48-210 and Wednesdays 13:45-15:15 in room 46-280 on the University of Kaiserslautern campus.
Program Analysis course at TU Kaiserslautern
The course meets Mondays 17:15-18:45 in room 48-379 on the University of Kaiserslautern campus.
More information about the course
Complexity Theory Course at TU Kaiserslautern
The course meets Mondays 15:30-17:00 at 46-280 and Wednesdays 13:45-15:15 at 46-268.
More information about the course
Three MPI-SWS papers accepted to POPL'17
- A promising semantics for relaxed-memory concurrency
- Relational cost analysis
- Thread modularity at many levels: a pearl in compositional verification
Rupak Majumdar will chair CAV 2017
CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis and synthesis methods for hardware and software systems. The CAV home page has more information.
Joel Ouaknine will chair LICS 2017
Neel Krishnaswami joins University of Cambridge as university lecturer
Congratulations, Neel!
Derek Dreyer awarded ERC Consolidator Grant

The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, ...
The European Research Council (ERC) is a pan-European funding body that supports cutting-edge research. It offers funding for groundbreaking research projects of the highest scientific quality across Europe, across all research areas. Talented researchers from all over the world can receive funding for excellent research in Europe. The ERC Consolidator Grant offers funding for researchers with 7 to 12 years of experience after achieving a PhD.
The RustBelt Project
A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.
Rust is a new language developed at Mozilla Research that marries together the low-level flexibility of modern C++ with a strong "ownership-based" type system guaranteeing type safety, memory safety, and data race freedom. As such, Rust has the potential to revolutionize systems programming, making it possible to build software systems that are safe by construction, without having to give up low-level control over performance.
Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art.
In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of "unsafe" code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems.
More
Joel Ouaknine joins the MPI-SWS faculty

In 2015, Joel was awarded an ERC Consolidator Grant, which provides almost 2 million euros of research funding over a period of five years. ...
In 2015, Joel was awarded an ERC Consolidator Grant, which provides almost 2 million euros of research funding over a period of five years. He is also the recipient of the 2010 Roger Needham Award, given annually "for a distinguished research contribution in Computer Science by a UK-based researcher within ten years of his or her PhD."
Joel will join MPI-SWS from the University of Oxford, where he is a Professor of Computer Science and Fellow of St John's College. Joel holds a BSc and MSc in Mathematics from McGill University, and received his PhD in Computer Science from Oxford in 2001. He subsequently did postdoctoral work at Tulane University and Carnegie Mellon University.
Sadegh Soudjani receives DIC Best PhD-Thesis Award
Aaron Turon receives SIGPLAN Dissertation Award
Rupak Majumdar receives POPL Most Influential Paper Award
Majumdar won the award for his 2004 paper, Abstractions From Proofs, which was coauthored with Thomas Henzinger, Ranjit Jhala, and Kenneth McMillan. ...
Majumdar won the award for his 2004 paper, Abstractions From Proofs, which was coauthored with Thomas Henzinger, Ranjit Jhala, and Kenneth McMillan. The paper introduced a technique to automatically find program abstractions using logical interpolation and showed the effectiveness of the technique in software verification.
Derek Dreyer wins funding from Microsoft Research
Ruzica Piskac wins Patrick Denantes Prize
Two MPI-SWS students receive Google Fellowships
Rupak Majumdar wins EAPLS and TODAES best paper awards
Rupak Majumdar and Zhenyue Long, along with Georgei Calin and Roland Meyer at TuKL, have received the ETAPS 2012 best paper award for their paper "Language-Theoretic Abstraction Refinement".
Rupak Majumdar has also received (along with Jason Cong, Bin Liu, ...
Rupak Majumdar and Zhenyue Long, along with Georgei Calin and Roland Meyer at TuKL, have received the ETAPS 2012 best paper award for their paper "Language-Theoretic Abstraction Refinement".
Rupak Majumdar has also received (along with Jason Cong, Bin Liu, and Zhiru Zhang) the 2012 ACM TODAES Best Paper Award for his 2010 TODAES article "Behavior-Level Observability Analysis for Operation Gating in Low-Power Behavioral Synthesis".
Rupak Majumdar wins PLDI most influential paper award
The ACM SIGPLAN Most Influential PLDI Paper Award is given each year for a paper that is ten years old and has been highly influential in the area of programming languages.
Rupak's 2001 paper, "Automatic Predicate Abstraction of C Programs," was coauthored with Thomas Ball, Todd Millstein, and Sriram Rajamani. The paper presented the predicate abstraction technology underlying the SLAM project. ...
The ACM SIGPLAN Most Influential PLDI Paper Award is given each year for a paper that is ten years old and has been highly influential in the area of programming languages.
Rupak's 2001 paper, "Automatic Predicate Abstraction of C Programs," was coauthored with Thomas Ball, Todd Millstein, and Sriram Rajamani. The paper presented the predicate abstraction technology underlying the SLAM project. The technology is now part of Microsoft's Static Driver Verifier in the Windows Driver Development Kit. This is one of the earliest examples of automation of software verification on a large scale and the basis for numerous efforts to expand the domains that can be verified.
Three new faculty to join MPI-SWS

We are pleased to announce that three new faculty will join MPI-SWS this fall.
Björn Brandenburg is joining us from the University of North Carolina at Chapel Hill (UNC), where he obtained his Ph.D. in computer science. Björn's research interests include multiprocessor real-time system, real-time synchronization protocols, and operating systems. Björn is the lead designer and developer of LITMUSRT, an extension of the Linux kernel for real-time scheduling and synchronization on multicore platforms.
...We are pleased to announce that three new faculty will join MPI-SWS this fall.
Björn Brandenburg is joining us from the University of North Carolina at Chapel Hill (UNC), where he obtained his Ph.D. in computer science. Björn's research interests include multiprocessor real-time system, real-time synchronization protocols, and operating systems. Björn is the lead designer and developer of LITMUSRT, an extension of the Linux kernel for real-time scheduling and synchronization on multicore platforms.
Deepak Garg is joining us from the Cybersecurity Lab (CyLab) at Carnegie Mellon University, where he was a post-doctoral researcher. He obtained his Ph.D. from Carnegie Mellon's Computer Science Department. His research interests are in the areas of computer security and privacy, formal logic and programming languages. He is specifically interested in logic-based models of secure systems and formal analysis of security properties of systems.
Ruzica Piskac is joining us from EPFL, where she has completed her Ph.D. in computer science. The goal of her research is to make software development easier and software more reliable via automated reasoning techniques. She is specifically interested in decision procedures, their combinations and applications in program verification and software synthesis.
Viktor Vafeiadis joins the MPI-SWS faculty

Viktor's research contributions include inventing new concurrent program logics (RGSep & deny/guarantee); developing automated verification tools (SmallfootRG & Cave) for proving correctness properties of concurrent algorithms; and verifying some particularly challenging algorithms manually (e.g., mcas), mechanically (e.g., fast congruence closure), or automatically (e.g., lazy set).
Viktor received his B.A. ...
Viktor's research contributions include inventing new concurrent program logics (RGSep & deny/guarantee); developing automated verification tools (SmallfootRG & Cave) for proving correctness properties of concurrent algorithms; and verifying some particularly challenging algorithms manually (e.g., mcas), mechanically (e.g., fast congruence closure), or automatically (e.g., lazy set).
Viktor received his B.A. degree in Computer Science in 2004 and his Ph.D. degree in Computer Science in 2008 both from the University of Cambridge. After that, he held post-doctoral research positions at Microsoft Research and at the University of Cambridge.
Rupak Majumdar joins the MPI-SWS faculty

Rupak's research spans the spectrum of formal verification techniques, ranging from theoretical foundations of logic and automata theory to practical software engineering tools that systematically analyze thousands of lines of code for programmer errors. In the field of software model checking, ...
Rupak's research spans the spectrum of formal verification techniques, ranging from theoretical foundations of logic and automata theory to practical software engineering tools that systematically analyze thousands of lines of code for programmer errors. In the field of software model checking, Rupak has made major contributions. Rupak, along with Ranjit Jhala, wrote the the model checker Blast, which is able to analyze over 100,000 lines of code for complex temporal properties. This achievement was a major milestone and proof of feasibility in the field of software verification and led to a flurry of academic and industrial activity in the area.
Rupak joins MPI-SWS from the University of California, Los Angeles, where he was on the faculty of the computer science department. Prior to that, Rupak received his Ph.D. degree in Computer Science from the University of California at Berkeley, and his B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur.
Robert Harper appointed as an external scientific member

The external scientific member appointment is a courtesy appointment, which acknowledges the member's scientific excellence, as well as his or her close collaboration and contribution to joint research projects with MPI-SWS faculty and researchers. ...
The external scientific member appointment is a courtesy appointment, which acknowledges the member's scientific excellence, as well as his or her close collaboration and contribution to joint research projects with MPI-SWS faculty and researchers.
Robert Harper has been a professor in the Computer Science Department at Carnegie Mellon University since 1988. He received his Ph.D. in Computer Science from Cornell University in 1985, and was a post-doctoral research fellow at the Laboratory for Foundations of Computer Science at Edinburgh University from 1985-1988. He is best known for his work on the design, definition, and implementation of Standard ML; the design and application of the LF logical framework; the type-theoretic foundations of modularity in programming languages; the use of typed intermediate languages for certified compilation; the co-invention of self-adjusting computation for dynamic algorithms; and the application of fundamental theory to practical software systems. His current interests include mechanization of the metatheory of programming languages, the integration of types and verification, and the application of programming language theory to computer security.
Umut Acar joins the MPI-SWS faculty

Such systems abound in many areas of computer science. For example, physical simulations often involve objects that move continuously over time, databases host and process data that changes over time (e.g., by introduction of new information records), ...
Such systems abound in many areas of computer science. For example, physical simulations often involve objects that move continuously over time, databases host and process data that changes over time (e.g., by introduction of new information records), and connectivity in networks and distributed systems changes as links go down or come alive.
Umut's primary research focus has been self-adjusting computation, where computations respond automatically to modifications to their data. With his collaborators, he designs languages for developing self-adjusting programs, researches techniques for analyzing their complexity, and evaluates the proposed techniques by considering problem domains such as computational geometry, machine learning, and scientific computing. Umut's other interests include parallel computing, databases, and design and implementation of high-level languages.
Umut Acar received his B.S. in Computer Science from Bilkent University-Turkey in 1997, his M.A. from University of Texas at Austin in 1999, and his Ph.D. from Carnegie Mellon University in 2004. Umut joins MPI-SWS from the Toyota Technological Institute of Chicago, where he was an assistant professor from 2005 to 2009.
Ashutosh Gupta and Andrey Rybalchenko win ETAPS best paper award
The EAPLS award goes to the best contribution in the area of programming languages among CC, ESOP, and TACAS—three member conferences of ETAPS, the European Joint Conferences on Theory and Practice of Software.
The award-winning paper describes the design and implementation of an automatic invariant generator that can be used in the verification of imperative programs. ...
The EAPLS award goes to the best contribution in the area of programming languages among CC, ESOP, and TACAS—three member conferences of ETAPS, the European Joint Conferences on Theory and Practice of Software.
The award-winning paper describes the design and implementation of an automatic invariant generator that can be used in the verification of imperative programs. The authors' new approach makes constraint solving—and hence invariant generation—more scalable by adding information obtained from static abstract interpretation as well as dynamic execution of the program.
ETAPS, established in 1998, is a confederation of five annual conferences, accompanied by satellite workshops and other events. It is a primary forum for academic and industrial researchers working on topics relating to Software Science. Previous EAPLS best paper award winners are listed at http://www.eapls.org/pages/topic_05_awards/.
Three new faculty to join MPI-SWS
Rodrigo Rodrigues will lead a research group on Dependable Systems. He obtained his Ph.D. from the Massachusetts Institute of Technology and joins us from the Instituto Superior Tecnico in Lisbon.
Derek Dreyer will lead a research group on Type Systems and Functional Programming. He obtained his Ph.D. from Carnegie Mellon University and joins us from the Toyota Technological Institute at Chicago. ...
Rodrigo Rodrigues will lead a research group on Dependable Systems. He obtained his Ph.D. from the Massachusetts Institute of Technology and joins us from the Instituto Superior Tecnico in Lisbon.
Derek Dreyer will lead a research group on Type Systems and Functional Programming. He obtained his Ph.D. from Carnegie Mellon University and joins us from the Toyota Technological Institute at Chicago.
Andrey Rybalchenko will lead a research group on Verification Systems. He previously held a post-doctoral position with Tom Henzinger at EPFL. He is the winner of the Otto-Hahn-Medal of the Max Planck Society.