Research Associate in Verification of Linear Dynamical Systems

The department has a new opening for a Research Associate in Verification of
Linear Dynamical Systems, working with Professor James Worrell, and funded by
an Established Career Fellowship from EPSRC. The overall goal of this proposal
is to develop techniques to solve fundamental computational problems arising
in the verification of discrete and continuous linear dynamical systems,
including Markov chains, linear recurrence sequences, linear while loops, and
linear differential equations.



You will develop algorithms to solve reachability, termination, and synthesis
problems for these models by combining a range of computational techniques,
including quantifier elimination and lattice reduction, and will use results
from number theory (particularly lower bounds in Diophantine approximation).
In cases where algorithms cannot be obtained, you will seek reductions from
known “hard” problems. The proposal aims to build on, and significantly
develop, recent progress of the PI and collaborators in solving long-standing
open problems in this area.



You should have a PhD (or be close to completion) in a relevant area of
science or related discipline, together with a document track record of the
ability to conduct and complete research projects in automated verification,
automata theory, dynamical systems, or algorithmic algebra and number theory.
Experience of independently managing a discrete area of a research project, or
of actively collaborating in the development of research articles for
publication is highly desirable.



The closing date for applications is 12.00 noon on Friday 13 July 2018.