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.

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.

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.

System Verification Lab (SVL)

As computing becomes increasingly integral to our societies, ensuring the correctness of IT systems is crucial. We explore various methods to formally model and verify computational systems, aiming to identify costly bugs and ensure correct implementations. Utilizing symbolic reasoning techniques from artificial intelligence, we realize automatic verification of large systems through a process known as model checking. Additionally, we develop new parallel and quantum algorithms to harness the capabilities of next-generation computing systems. In partnership with industry, we investigate stochastic processes, particularly those involved in the risk analysis of power grid infrastructure and the optimization of engineering processes.

Semantics, Types & Logic (STyLo)

The work of the STyLo group revolves around correctness of systems by construction, and the verification and analysis of systems. To implement systems that fulfil desired properties by construction, one needs languages that statically guarantee these properties. We focus on using type systems, since they enable compositional reasoning. An understanding of the induced behaviour of such languages is gained through their semantics, which we develop with tools from category theory and other areas of mathematics. Interestingly, the same tools that we use to construct and analyse type systems can also be used as the foundation of logical deduction systems. Such deduction systems underlie the verification and analyis of systems, both in the form of computer-assisted proofs and in automatic deduction. We choose to focus on compositional and computer-assisted reasoning because they are key to handling the complexity of constructing and analysing large systems.

Logic and computation are inseparable strands, if viewed through the right lens. In the STyLo group, we use category theory, type theory and language semantics as such lenses to structure our work and gain new insights in how the strands can be developed. The benefit of using and developing abstract theories is that these are readily applicable to systems in various areas of, for example, computer science, physics, biology and chemistry.

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.

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.