Verification techniques are used for proving that a system meets its requirements and specifications. Our group works at all aspects of this exciting topic. We have expertise in many different techniques that are applied in the formal analysis of systems, spanning model-checking and run-time verification, automata and game theory, resolution and tableaux, and algebraic methods. We study verification, optimisation, and control problems for reactive, hybrid, and stochastic systems with varying degrees of independent agents with collaborative (swarms) and competitive goals.

The group is led by Dr Alexei Lisitsa