Theory

Many important topics in computer science, such as the correctness of software, the efficiency of algorithms and the modeling of complicated systems, depend on sound theoretical underpinnings. In the Theory group, we study these fundamental building blocks and develop verification methods to prove system correctness, new (quantum) algorithms and fundamental models of concurrency and infinite-state systems.

Algorithms

We develop combinatorial algorithms, for example for use in different types of games, with a special emphasis on algorithms that can be applied in biology, such as massive string matching. We also work on scalable algorithms for analyzing networked systems in the real world. Examples include computational approaches for computing distance measures such as the diameter, as well as efficiently counting characteristic graph patterns.

Bio-inspired Computing

We investigate reaction systems, a novel computational model gleaned from the biochemical reactions taking place in living cells and information processing in nature. Other formal models inspired by molecular reactions within cells are membrane and tissue systems. For these we develop a causality semantics following a Petri net based approach. Another non-traditional approach to computing is DNA computing. This is based on molecular biology hardware. We use algebraic and combinatorial techniques to model and analyze these computational processes, like the rearrangement of genes.

Concurrent Systems

In modern information systems, a large number of different components are often active simultaneously. This phenomenon - known as concurrency - underlies not only the functioning of computer systems but of any system in which many processes take place at the same time. It leads to a huge variety of complicated interactions that affect the overall functioning of the system. The aim of our research of concurrent systems is to understand and model these interactions and describe their effect. We investigate Petri nets as well as other models of concurrent and distributed systems, like team automata. Our focus is on semantical aspects, synthesis, and formal analysis and verification techniques. This research profits from our expertise and ongoing theoretical research in the fields of mathematical structures, logic, formal languages and automata. We apply our insights to and are motivated by biological systems, hardware (asynchronous circuits), and business protocols (e.g., groupware and financial markets). In collaboration with CWI, we investigate the development, implementation, and applications of Reo, an exogenous coordination model for construction of coordinating connectors in distributed, mobile, and dynamically reconfigurable component-based systems.

Quantum Lab

Quantum computing is a novel paradigm for computation, which is nearing real-world impact with the coming generation of limited, but nonetheless powerful quantum devices. We study and develop novel algorithms for general quantum computers,  specialized algorithms for near-term machinery, and hybrid algorithmic methods combining classical and quantum computation. In particular, we focus on the development of quantum algorithmic foundations for heuristic computing and machine learning. Together with the Applied Quantum Algorithms (aQa) initiative in Leiden, we also study the application of our methods to real-world problems, and the integration of theory, experiment and real-world application.

Systems Modelling Lab (SML)

Mathematical models of software systems enable characterizations, abstractions, simulations, and analysis of complex software during its development. The use of mathematical techniques from the fields of algebra, coalgebra, automata theory, logic, type theory, and category theory allows for formal specification and analysis, which contribute to the correct design and implementation of a software system. We develop new mathematical techniques that are necessary for dealing with current and future features of software systems. Furthermore, we develop rigorous models and powerful algorithms for reasoning about modern object-oriented programs, concurrent and probabilistic systems, coordination languages, and software-defined networks. We also explore the application of the modelling and reasoning techniques to other systems that arise outside of computer science.

System Verification Lab (SVL)

The correctness of computational systems is of great importance to our society, since it becomes ever more reliant on the benefits of computing. We study a range of approaches to formally model and verify computational systems to detect costly bugs and realize correct implementations. With symbolic reasoning techniques from Artificial Intelligence, we enable the fully automatic verification of larger systems through a method called model checking. In collaboration with the Concurrent Systems Lab, we develop reduction techniques to the same end. And in collaboration with the Quantum and Algorithms Labs, we develop new quantum and parallel algorithms to exploit the power of next-generation computing systems for verification. The added computational power is also necessary to analyze the behaviour of stochastic processes, such as those underlying the risk analysis of power grid infrastructure. In collaboration with industry, this forms another application area for our research.