Programming Languages and Verification

As software becomes both more complex and more deeply integrated into daily life, it is critical to ensure that it works correctly. This area examines the principles, design, and implementation of programming languages, developing techniques and tools for analysis, testing, and verification of programs against correctness specifications.

Groups and Researchers in this Field


Information Security and Cryptography

Michael Backes is a computer science professor at Saarland University, Director of the Center for IT-Security, Privacy, and Accountability, a Max Planck Fellow of the Max Planck Institute for Software Systems, and a Principal Investigator and Vice-Coordinator of the Cluster of Excellence on Multimodal Computing and Interaction. He leads the Information Security & Cryptography group, focusing on aspects of IT security and privacy, from design, analysis, and verification of protocols and systems, mechanisms for protecting end-user privacy, and research on new attack vectors to universal solutions in software and network security. Backes’ current main research focus is on the ERC Synergy Grant imPACT, which aims to provide foundations for privacy, accountability, compliance, and trust on the Internet of the future. Read more

Michael Backes

Michael Backes

MPI-SWS, Max Planck Fellow

Personal Website

Automated Verification and Approximation

Eva Darulova leads a research group at the Max Planck Institute for Software Systems. Her interests lie in the area of automated verification and synthesis for numerical programs. One difficulty in verifying numerical computations is the inherent mismatch between the continuous nature of much of mathematics and physical processes versus the discrete implementation on today’s digital computers. Reliably controlling accuracy is not enough; performance and energy efficiency have also become key design constraints for most applications. As these objectives often conflict, an acceptable tradeoff must be found. The goal of Eva’s research is to develop techniques and tools for automated reasoning about numerical programs, thus helping scientists and engineers write correct, accurate, and efficient software. Read more

Eva Darulova

Eva Darulova

MPI-SWS, Faculty

Personal Website

Foundations of Programming

Derek Dreyer leads the Foundations of Programming group at the Max Planck Institute for Software Systems. The group focuses on the design, semantics, verification, and implementation of modern programming languages and systems. Topics of study have included advanced type systems for modular programming and verification; Kripke models and separation logics for reasoning about higher-order, imperative, and concurrent programs; and compositional compiler certification. Derek is interested in developing a “realistic” theory of modularity—figuring out how we can build and reason modularly about programs that use features like fine-grained concurrency, higher-order state, recursive linking, dependent types, or self-modifying assembly code, meaning traditional semantic and verification techniques cannot account for them. Read more

Derek Dreyer

Derek Dreyer

MPI-SWS, Faculty

Personal Website

Computer Security Group

Deepak Garg’s interests include computer security and privacy, formal logic, and programming languages. He is head of the Foundations of Computer Security group, associated with both the Security & Privacy and the Programming Languages & Verification research areas at the Max Planck Institute for Software Systems. The group’s current projects investigate tracking and controlling flows of sensitive information through Web browsers, using type systems to statically estimate the asymptotic complexity of incremental runs of programs, creating mechanisms to enforce data protection policies across multiple system infrastructure layers, extending separation logics to reason about security protocols, and developing foundations and algorithms for temporal logic-based privacy audits of legal compliance, among others. Read more

Deepak Garg

Deepak Garg

MPI-SWS, Faculty

Personal Website

Rigorous Software Engineering

Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems, where he leads the Rigorous Software Engineering group. His main research interests include verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. His group investigates both foundational principles and practical tools for the design and analysis of computer systems. Some recent research directions have included methodologies and tools for the automated co-design of embedded controllers and their implementations, foundations of robustness for hybrid systems, scalable tools for coverability analysis of Petri nets, algorithms for the analysis of infinite-state systems, and verification of asynchronous programs. Read more

Rupak Majumdar

Rupak Majumdar

MPI-SWS, Faculty

Personal Website

Foundations of Algorithmic Verification

Joel Ouaknine is a Scientific Director at the Max Planck Institute for Software Systems, where he leads the Foundations of Algorithmic Verification group. He also holds secondary appointments at Saarland University and Oxford University. His research interests span a range of topics broadly connected to algorithmic verification and theoretical computer science. His group's recent focus has been on decision and synthesis problems for linear dynamical systems (both continuous and discrete), making use among others of tools from number theory, Diophantine geometry, and real algebraic geometry. Other interests include the algorithmic analysis of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, synthesis problems, complexity), logic and applications to verification, automated software analysis, and concurrency. Read more

Joel Ouaknine

Joel Ouaknine

MPI-SWS, Faculty

Personal Website

Arithmetic Reasoning

Thomas Sturm leads the Arithmetic Reasoning research area within the Max Planck Institute for Informatics’ Automation of Logic group. Arithmetic reasoning covers the study of first-order logic and arithmetic in theory and practice. This research area focuses on the design of new and the extension and optimization of existing arithmetic reasoning procedures, as well as on their application in problems from various scientific disciplines like chemistry, systems biology, and physics. Recent results include advancements in quantifier elimination procedures over the reals, compiler optimization, linear integer programs in verification systems, and theory-solving via superposition. In ongoing research, they aim to further extend the applicability of their implementations as well as their methods in automated reasoning. Read more

Thomas Sturm

Thomas Sturm

MPI-INF, Senior Researcher

Personal Website

Software Analysis and Verification

Viktor Vafeiadis leads the Software Analysis and Verification research group at the Max Planck Institute for Software Systems. The group’s research concerns the development of mathematical theories and tools for formally reasoning about software. It aims to improve software quality by making it possible to build provably correct software components. This involves coming up with rigorous mathematical specifications of software components, developing custom proof techniques for proving adherence to those specifications, and improving the underlying general-purpose verification infrastructure. Much of their work focuses on reasoning about concurrent programs; another important aspect of their work concerns the Coq interactive theorem prover and improving its applicability for reasoning about software. Read more

Viktor Vafeiadis

Viktor Vafeiadis

MPI-SWS, Faculty

Personal Website

Automation of Logic

Christoph Weidenbach leads the Automation of Logic research group at the Max Planck Institute for Informatics. The group’s work ranges from basic research on (new) logics and their automation up to applications in research and industry. Topics of interest include propositional and first-order logics and their combination with theories, arithmetic, decidable fragments for knowledge representation and reasoning, and fragments of higher-order logics. Results are reflected in system development including prototypical reasoning support for higher-order systems, as well as reasoning engines that are deployed in industrial practice. Example applications are verification of hardware and software, distributed systems analysis, query answering with respect to knowledge bases, product modeling and optimization, and biochemical process analysis. Read more

Christoph Weidenbach

Christoph Weidenbach

MPI-INF, Senior Researcher

Personal Website