Algorithms, Theory, Logic

This field investigates a range of theoretical and practical aspects of algorithmics. Considering all aspects of the process holistically—from analyzing the efficiency and the quality of the solutions, to developing provably efficient and correct software, to packaging and releasing this software—helps to inform the research as well as benefit the community.

Groups and Researchers in this Field


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

Foundations of Computer Security

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

Algorithmic Game Theory

Martin Hoefer is head of the Algorithmic Game Theory group in the Algorithms and Complexity Department at the Max Planck Institute for Informatics. Problems studied by the group usually involve optimizing some goal function while dealing with selfish agents that may have separate and conflicting goals, and that may lie in order to improve their own goal function. Algorithmic mechanism design, which lies at the intersection of economic game theory and computer science, seeks to ensure that it is in the best interest of the agents to tell the truth. The group also examines the price of anarchy and price of stability for various problems. The future of much of the complex technology being developed today depends on our ability to ensure that participants cooperate despite their diverse goals and interests. Read more

Martin Hoefer

Martin Hoefer

MPI-INF, Senior Researcher

Personal Website

Discrete Optimization

Discrete optimization problems are ubiquitous. Whenever there is a choice between several possibilities, there is an inherent optimization problem. Our core competence in this area is to recognize such optimization problems, to establish mathematical models, to tackle them by state-of-the-art methods, and to invent new techniques to obtain satisfactory results.  Our research is application-driven. This also includes inter-disciplinary research with collaborators from engineering, physics, chemistry, biology, economics, etc. Read more

Andreas Karrenbauer

Andreas Karrenbauer

MPI-INF, Senior Researcher

Personal Website

Theory of Distributed Systems

Christoph Lenzen coordinates the Theory of Distributed Systems research area in the Algorithms and Complexity Department at the Max Planck Institute for Informatics. Broadly, distributed computing concerns systems of multiple agents that act based on local information. Typical problems require agents to collaboratively solve a task quickly, despite limits on communication, faults, or inaccurate data. The group’s approach is largely based on tools of theoretical computer science. They devise abstract models to capture problems’ central challenges, and prove upper and lower bounds on the complexity of solutions in terms of the amount of communication, number of faults that can be tolerated, etc. They also seek to provide prototype implementations of their algorithms, which may then form a basis for applications. Read more

Christoph Lenzen

Christoph Lenzen

MPI-INF, Senior Researcher

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

Algorithms and Complexity

Kurt Mehlhorn is known for many research contributions in a wide variety of areas, among them algorithms, complexity, and optimization, as well as for his work on software including LEDA. In addition to being a director of the Max Planck Institute for Computer Science, he heads its Algorithms & Complexity Department, which takes a holistic approach to studying theoretical and practical aspects of modern algorithmics: from designing new algorithms and algorithmic techniques, analyzing their efficiency and the quality of their solutions, and developing provably efficient and correct software, to packaging the programs in software libraries. He is also a Principal Investigator at the Cluster of Excellence on Multimodal Computing and Interaction, and a director of the Indo-German Max Planck Center for Computer Science. Read more

Kurt Mehlhorn

Kurt Mehlhorn

MPI-INF, Scientific Director

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

Geometry, Topology, and Algebra

Michael Sagraloff coordinates the Geometry, Topology, and Algebra research area in the Algorithms and Complexity Department at the Max Planck Institute for Informatics. A common theme here is the quest for theoretical guarantees; this includes the complexity analysis of algorithms, but also the design of certified yet efficient algorithms for problems usually tackled through heuristical approaches without strict guarantees. He also investigates structural properties of geometric and topological structures, often in relation to upper and lower bounds of algorithmic approaches. An important part of his work involves applying his algorithms “in the field”, through implementation, experimental evaluation, application to real-world problems, and integration into mature software packages. Read more

Michael Sagraloff

Michael Sagraloff

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

Combinatorial Optimization

Andreas Wiese coordinates the Combinatorial Optimization area in the Algorithms & Complexity Department at the Max Planck Institute for Informatics. Many real-world applications can be formulated as combinatorial optimization problems, i.e. finding the best solution(s) in a finite set. A well-known example is the traveling salesman problem, but there are many other important problems in various settings like routing, scheduling, graph theory, packing, or throughput maximization. The group applies a variety of methods to tackle such problems, for instance approximation algorithms, integer programming, fixed-parameter algorithms, and combinatorial algorithms. They also develop new techniques to improve efficiency, obtain sharper analyses, and tighten upper and lower bounds on the computational complexity of various optimization problems. Read more

Andreas Wiese

Andreas Wiese

MPI-INF, Senior Researcher

Personal Website