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
Principles of Security and Privacy
Gilles Barthe's research interests lie in the areas of programming languages and program verification, software and system security, cryptography, formal methods and logic. His goal is to develop foundations and tools for reasoning about security and privacy properties of algorithms and implementations. His recent work focuses on building relational verification methods for probabilistic programs and on their applications in cryptography and privacy. He is also interested in provably secure countermeasures against side-channel attacks. Read more
Karl Bringmann leads the group Fine-Grained Complexity and Algorithms in the Algorithms and Complexity department at the Max Planck Institute for Informatics. He is interested in the inherent time complexity of combinatorial problems. Specifically, which problems can be solved in near-linear time, which require quadratic time, etc.? Since NP-hardness is too coarse to answer such questions, the modern approach is to prove conditional lower bounds via fine-grained reductions from certain hardness assumptions; this approach is called fine-grained complexity theory. Karl’s group develops this theory and uses a combination of fine-grained lower bounds and algorithm design to determine the optimal time complexity of various problems from computational geometry, stringology, graph theory, and optimization. Read more
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
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
Philipp Hennig holds the Chair for the Methods of Machine Learning, and is an adjunct scientist at the Max Planck Institute for Intelligent Systems. He studied Physics in Heidelberg, Germany and at Imperial College, London, before moving to the University of Cambridge, UK, where he attained a PhD in the group of Sir David JC MacKay with research on machine learning. Since this time, he is interested in connections between computation and inference. With international collaborators, he helped establish the field of probabilistic numerics. His research was supported, among others, by the Emmy Noether Programme of the German Research Union (DFG), an independent Research Group of the Max Planck Society, and a Starting Grant of the European Commission. Read more
Cătălin Hrițcu is a tenured faculty member at the Max Planck Institute for Security and Privacy (MPI-SP). He is particularly interested in security foundations (secure compilation, compartmentalization, memory safety, security protocols, information flow), programming languages (program verification, proof assistants, dependent types, formal semantics, mechanized metatheory, property-based testing), and the design and verification of secure systems (reference monitors, secure compilation chains, tagged architectures). He was awarded an ERC Starting Grant on formally secure compilation and is also actively involved in the design of the F* verification system. Read more
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
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
Giulio Malavolta is a tenure-track faculty at the Max Planck Institute for Security and Privacy (MPI-SP). He is primarily interested in theoretical and applied aspects of cryptography and his work often intersects with other disciplines such as quantum computing, concurrent systems, cryptocurrencies, and game theory. His recent work focuses on establishing new feasibility results for cryptographic schemes with advanced functionalities. Read more
Michael Muehlebach is leading the independent research group Learning and Dynamical Systems at the Max Planck Institute for Intelligent Systems in Tuebingen, Germany. He is interested in a wide variety of subjects, including machine learning, dynamics, control, and optimization. Some of his recent work deals with large-scale constrained optimization in a machine learning context, stochastic minimax optimization, adaptive decision-making and reinforcement learning. While rigorous theory and mathematical analysis forms the basis of his research, he also likes to evaluate his algorithms in experiments with real-world cyber-physical or robotic systems, such as balancing robots or flying vehicles. Throughout his career Michael has received numerous awards, such as the ETH Medal and the HILTI prize for innovative research, and he was awarded the Branco Weiss and Emmy Noether Fellowship. Read more
Danupon Nanongkai will be joining MPI-INF as a director in July 2022. The research of his department is broadly on algorithms and complexity theory — developing algorithms with better, provable, performance guarantees using the power of mathematics. His research focuses on efficient graph (network) algorithms across different models of computation. Examples include improving classic textbook algorithms and developing algorithms on distributed networks, streams of graph data, and dynamically changing input graphs. Read more
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
Anne-Kathrin Schmuck is an independent research group leader at the Max Planck Institute for Software Systems in Kaiserslautern, Germany, funded by the Emmy Noether Programme of the German Science Foundation (DFG). Her research is driven by the goal to significantly expand the applicability of fully automated synthesis tools to reliable cyber physical system design. Her work draws inspiration from both Control Theory and Computer Science and centers around Reactive Synthesis, Supervisory Control Theory, Abstraction-Based Controller Synthesis, and Hierarchical Control. Recently, she has developed lazy abstraction techniques where abstract automata models of continuous system dynamics are generated lazily to enable efficient controller synthesis for discrete mission tasks. Further, she is developing contract-based distributed synthesis methods to safely coordinate multiple system components. Read more
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
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
Georg Zetzsche leads the Models of Computation research group at the Max Planck Institute for Software Systems. The group studies abstract models of computations, how to analyze them algorithmically, and how to use them to represent program behavior. Topics of interest are therefore decidability, complexity, and expressiveness of infinite-state systems. The studied models of computation include concurrent systems such as Petri nets and other counter machines, but also models of recursion such as (higher-order) pushdown automata. The group applies methods from automata theory, formal languages, and logic, but also semigroup and group theory. Currently in focus are the synthesis of finite-state abstractions of infinite-state systems, such as closure computation and separability problems, and also algorithmic problems for infinite groups. Read more
