Application deadline: 31st March 2024
The main goal of the field of algorithmic verification is to come up with methods that would help us ensure that the systems we design do not exhibit any erroneous behaviour. This is a project belonging to the field of algorithmic verification, focused on verifying the correctness of certain infinite-state systems.
We will generally strive to design algorithms for analysing dynamical systems such as piecewise affine maps [1], linear recurrence sequences [2], and related objects.
The existence of algorithms in this area is typically demonstrated using results from (algebraic) number theory. As a consequence, a strong background in mathematics and theoretical computer science is highly desired. On the other hand, we will also implement proof-of-concept tools for the algorithms that we design, therefore interest in programming is appreciated.
For a better idea of the themes I am interested in, see: https://edon.github.io/publications_theme.html
Supervisor: Edon Kelmedi - e.kelmendi@qmul.ac.uk
[1] https://arxiv.org/abs/2301.09752
[2] https://arxiv.org/abs/2109.14432