Postdoctoral position in verification of linear dynamical systems, Oxford (England)

A vacancy has arisen for a full-time researcher on the topic of Verification of Linear Dynamical Systems, led by Professor James Worrell at the Department of Computer Science, University of Oxford. This is a fixed-term position for 2 years, starting Jan 2017 or as soon as possible thereafter.

The overall aim of the project is to solve fundamental computational problems in the verification of discrete and continuous linear dynamical systems, including Markov chains, probabilistic automata, linear recurrence sequences, linear while loops, and linear differential equations. The project aims to build on recent progress in the area, developing decision procedures to solve reachability, termination, and synthesis problems. The methodology will combine a range of computational techniques, including quantifier elimination and lattice reduction, as well as results from number theory (particularly Diophantine approximation).