Concurrency, that is, the simultaneous use of multiple units of computation on a common task, can significantly speed up computation, but at the cost of making it significantly more complicated. Despite its complexity, concurrency is now pervasive, from hardware featuring multiple units of computation called cores, to the concurrent programs running on these machines, to the so-called distributed systems that run across thousands of computers all over the world. The ubiquity and critical role of concurrency, together with the unique scaling challenges it raises, calls for new methods and tools to increase safety and reliability. 

Research in our section tackles all layers of computer systems where concurrency is, from hardware (for example the Arm and RISC-V architectures), including so-called relaxed concurrency, whereby not all units of computations have the same view of what has happened, to concurrency in programming languages (for example C, C++, and Go), and to distributed systems and databases. Our research involves modelling work in collaboration with industry, developing efficient model-checking algorithms and bug-finding tools, and designing verification methods. 

Modelling of hardware and programming languages helps programmers work with confidence so they can build reliable and secure systems. Bug-finding tools make it possible for working programmers to prototype their ideas faster. Verification clarifies the conditions under which certain programming idioms are guaranteed to work.