Graphs form a mathematical model of a network of nodes joined by links. Methods to model and approximate large graphs find applications in analyzing complex networks such as Facebook and LinkedIn. Graph algorithms are used to solve problems where the input can be encoded by a graph, which include navigation, routing and scheduling problems.

Graham Cormode, Alexander Tiskin, Dan Kral.

It is not always possible or practical to compute the best possible solution to an optimization problem because, initially, the input may not be fully known. Approximation and online algorithms deliver solutions that are guaranteed to have cost within a certain percentage of the optimum and they do so in a timely manner.

Graham Cormode, Matthias Englert, Dan Kral.

Model checking is the dominating approach to deep bug discovery in critical systems. Based on automata theory, model checking is nowadays a key part of the development process at companies including Facebook, Intel and Microsoft.

Marcin Jurdziński, Ranko Lazić, Andrzej Murawski.

In our cutting-edge research on computer-aided verification, algorithm design meets game theory to produce optimal procedures and complexity bounds for analysing and synthesising massively concurrent systems that operate on very large data.

Marcin Jurdziński, Ranko Lazić, Andrzej Murawski.

Streaming and summarization algorithms study what can be computed when the data stored is sublinear in the size of the input. Techniques developed here have applications to making the analysis of large data more scalable.

Graham Cormode, Artur Czumaj, Dan Kral.

Efficient algorithms on strings (sequences) of characters are essential for applications that include web indexing and searching, text processing and bioinformatics.

Artur Czumaj, Alexander Tiskin.