Loughborough University is a top-ten rated university in England for research intensity (REF2014) and an outstanding 66% of the work of Loughborough’s academic staff who were eligible to be submitted to the REF was judged as ‘world-leading’ or ‘internationally excellent’, compared to a national average figure of 43%. In choosing Loughborough for your research, you’ll work alongside academics who are leaders in their field. You will benefit from comprehensive support and guidance from our Doctoral College, including tailored careers advice, to help you succeed in your research and future career. Nature of work: This is a theoretical project that might potentially involve some design, implementation and testing of algorithms. Area: Formal verification; automata theory; finite semigroups; finite model theory; logic Potential implications: Potential results might lead to new and promising methods in formal verification. They could, hence, improve existing algorithms and their implementations, which would allow certain verification tasks to be performed more efficiently. It might also be possible to use techniques from logic and verification for solving problems in algebra. It is therefore anticipated that, if successful, the project would have significant academic as well as applied impact. Formal verification aims at rigorously proving that a system satisfies some specification. Systems can be modelled using abstract machines and specifications are given using logic descriptions. There exist various possibilities to solving verification problems. A quite general approach is to translate both the system and the specification into a common data structure with desirable effective closure properties. The algorithms for these closure properties can then be used for deciding whether the system satisfies the specification. The aim of this project is to use homomorphisms to finite semigroups as such a data structure. One advantage is that it allows efficient minimisation, even in cases where no such techniques are known for other data structures. There are certain downsides to finite semigroups, and it would be interesting to get a better understanding of the situations in which efficient minimisation makes up for these downsides. In particular, one would need to investigate the complexity and efficient algorithms for the various closure properties of finite semigroups.