Programming Languages & Verification

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:
  • 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

December 2017
Maria Christakis, an MPI-SWS faculty member, has received a Facebook Faculty Research Award. The award is given in recognition of Maria's work on combining static and dynamic program analysis, which is of particular relevance to Facebook as they are developing sophisticated program analysis tools to handle real-world code.

Two MPI-SWS faculty awarded DFG grants

December 2017
Two MPI-SWS faculty members have received 3-year research grants from DFG, the German Research Organization.

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

October 2017
David Swasey, Deepak Garg, and Derek Dreyer have won a Distinguished Paper award at the 2017 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2017) for their paper "Robust and Compositional Verification of Object Capability Patterns."

Distinguished Paper awards are given to about 10% of papers at OOPSLA.

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

June 2017
MPI-SWS researchers made a very strong showing at PLDI and ECOOP in Barcelona this year.  They received two Best Paper Awards, one from PLDI and one from ECOOP, for the following two papers:

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

June 2017
Maria Christakis joins the institute as a tenure-track faculty member, effective Oct 16, 2017. Maria’s goal is to develop theoretical foundations and practical tools for building more reliable and usable software and increasing developer productivity. She is mostly interested in software engineering, programming languages, and formal methods. Maria particularly likes investigating topics in automatic test generation, software verification, program analysis, and empirical software engineering. Her tools and techniques explore novel ways of writing, specifying, verifying, testing, and debugging programs in order to make them more robust while at the same time improving the user experience.

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.

Principles of Cyber-Physical Systems Course at TU Kaiserslautern

April 2017
Sadegh Soudjani is teaching Principles of Cyber-physical Systems at the University of Kaiserslautern in Summer 2017.

The course meets Tuesdays 11:45-13:15 and Thursdays 10:00-11:30 in 11-260.

Advanced Automata Theory Course at TU Kaiserslautern

April 2017
Rupak Majumdar and Daniel Neider are co-teaching Advanced Automata Theory at the University of Kaiserslautern in the Summer 2017 semester.

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

November 2016
Rayna Dimitrova is teaching Program Analysis at the University of Kaiserslautern in the Winter 2016-17 semester.

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

November 2016
Rupak Majumdar is teaching Complexity Theory at the University of Kaiserslautern in the Winter 2016-17 semester.

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

October 2016
Three papers from MPI-SWS were accepted to ACM POPL 2017:
  • 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

October 2016
Rupak Majumdar and Viktor Kuncak (EPFL) are co-chairs of the 29th International Conference on Computer-Aided Verification (CAV 2017), to be held between July 22 and 28, 2017 in Heidelberg, Germany.

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

October 2016
Joel Ouaknine is the Program Chair of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), to be held between 20 and 23 June, 2017 in Reykjavik. The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed.

Neel Krishnaswami joins University of Cambridge as university lecturer

July 2016
Neel Krishnaswami, a former postdoc in Derek Dreyer's group at MPI-SWS, will be joining the University of Cambridge Computer Laboratory as a University Lecturer.

Congratulations, Neel!


Derek Dreyer awarded ERC Consolidator Grant

April 2016
Derek Dreyer, head of the MPI-SWS Foundations of Programming group, has been awarded an ERC Consolidator Grant. Over the next five years, his project "RustBelt: Logical Foundations for the Future of Safe Systems Programming" will receive almost 2 million euros, which will allow the group to develop rigorous formal foundations for the Rust programming language.

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.


Joel Ouaknine joins the MPI-SWS faculty

March 2016
Joel Ouaknine joins the institute's faculty as a scientific director, effective Aug 1, 2016. Joel's research interests include the automated verification of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, synthesis problems, complexity), logic and applications to verification, decision and synthesis problems for linear dynamical systems, automated software analysis, concurrency, and theoretical computer science.

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 wins DIC Best PhD-Thesis Award

March 2015
MPI-SWS postdoctoral fellow Sadegh Soudjani has been awarded the DISC Best PhD-Thesis Award for the best PhD thesis defended in 2014 in the Netherlands in the area of systems and control. Dr. Soudjani received the award for the excellent quality of his PhD Thesis "Formal Abstraction for Automated Verification and Synthesis of Stochastic Systems" for which he obtained the doctoral degree at Delft University of Technology in November.

Aaron Turon receives SIGPLAN Dissertation Award

June 2014
Aaron Turon, a postdoc in Derek Dreyer's Foundations of Programming Group, has received the 2014 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award for his PhD thesis, "Understanding and Expressing Scalable Concurrency", which he completed at Northeastern University in 2013 under the supervision of Mitch Wand. This international award is presented annually to the author of the outstanding doctoral dissertation in the area of Programming Languages. Aaron has recently joined Mozilla Research in San Francisco, where he is a member of the development team for the Rust programming language.

Rupak Majumdar wins Most Influential Paper Award

January 2014
MPI-SWS faculty member Rupak Majumdar has been selected as the winner of this year's POPL (Principles of Programming Languages) Most Influential 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.

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

May 2013
A research project proposed by MPI-SWS faculty member Derek Dreyer has been selected for a 2013 Microsoft Research PhD Scholarship. The project is entitled "Compositional Verification of Scalable Joins by Protocol-Based Refinement". Each year Microsoft selects approximately twenty projects to fund, based on proposals from research institutions across Europe, Africa, and the Middle East. The Scholarship funds a PhD student for three years.

Ruzica Piskac wins Patrick Denantes Prize

September 2012
Ruzica Piskac, an MPI-SWS faculty member, has been awarded the 2012 Patrick Denantes Prize for her dissertation titled "Decision Procedures for Program Synthesis and Verification." The prize is awarded annually to the most outstanding master's, doctoral or post-doctoral research project within the school of computer and communication sciences at EPFL.

Two MPI-SWS students receive Google Fellowships

June 2012
Fourth-year PhD student Georg Neis won a 2012 Google PhD Fellowship for his work in Programming Technology. First-year PhD student Ezgi Cicek was awarded an Anita Borg Scholarship. They join MPI-SWS PhD student Juhi Kulshrestha, who received a 2011 Google Fellowship for her work in social networking.

Rupak Majumdar wins EAPLS and TODAES best paper awards

June 2012
MPI-SWS faculty Rupak Majumdar, along with his coauthors, has received two best paper awards: the EAPLS 2012 best paper award and the 2012 ACM TODAES best paper award.

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

August 2011
MPI-SWS faculty Rupak Majumdar has received the ACM SIGPLAN Most Influential PLDI (Programming Language Design and Implementation) Paper Award for 2011.

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

July 2011

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

October 2010
Viktor Vafeiadis joins the institute's faculty, starting in October 2010. Viktor's research interests are in software analysis and verification, programming languages, programming logics, and concurrency.

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.

Robert Harper appointed as an external scientific member

June 2010
Robert Harper has been appointed as the institute's first external scientific member. Dr. Harper is a Professor of Computer Science at Carnegie Mellon University, where he conducts research on programming language design and implementation. Bob will be visiting the institute in Summer 2010.

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

January 2010
Umut Acar joins the institute's faculty, starting in January 2010. Umut's research interests are in language and algorithm design and implementation, particularly for dynamic systems that interact with changing data from various sources, such as users and the physical environment.

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

July 2009
MPI-SWS PhD student Ashutosh Gupta and and faculty Andrey Rybalchenko, along with Rupak Majumdar (UCLA), have received the EAPLS best paper award for their TACAS'09 paper "From Tests to Proofs."

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