Applications of finite semigroups in formal verification PhD

Department(s):
Computer Science
Entry requirements:
2:1+
Full-time:
3 years
Part-time:
not available
Reference number:
MK/CO/2018
Start date:
01 October 2018
Is funding available?
Yes
UK/EU fees:
N/A
International fees:
TBC
Location:
Loughborough
Application deadline:
16 February 2018

Achievements

4th

in the UK for Computer Science

Guardian University Guide 2018

Top 20

in the UK for Computer Science

The Complete University Guide 2018

75%

of research impact rated 'internationally recognised' or higher

Overview

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. 

Project detail

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.

Supervisors

Primary supervisor: Manfred Kufleitner

Secondary supervisor: Daniel Reidenbach

Find out more

For further project details email Manfred Kufleitner or register your interest and ask us a question.

To find out more about postgraduate research in the School of Science please visit our website.

Entry requirements

Applicants should have, or expect to achieve, at least a strong 2:1 Honours degree (or equivalent) in Computer Science, Mathematics or a related subject.

Applicants must meet the minimum English Language requirements, details available on the website.

Fees and funding

UK/EU:
N/A
International:
TBC

Tuition fees cover the cost of your teaching, assessment and operating University facilities such as the library, IT equipment and other support services. University fees and charges can be paid in advance and there are several methods of payment, including online payments and payment by instalment. Special arrangements are made for payments by part-time students.

This studentship will be awarded on a competitive basis to applicants who have applied to this project and/or any of the advertised projects prioritised for funding by the School of Science.

The 3-year studentship provides a tax-free stipend of £14,553 per annum (in line with the standard research council rates) for the duration of the studentship plus tuition fees at the UK/EU rate.  International (non-EU) students may apply however the total value of the studentship will be used towards the cost of the International tuition fee in the first instance.

How to apply

All applications should be made online. Under programme name, please select ‘Computer Science’.

Please quote reference number: MK/CO/2018

Application details

Reference number: MK/CO/2018
Application deadline: 16 February 2018
Start date: 01 October 2018

Explore