Skip to main content

Fully Funded Doctoral Studentship in Machine Learning Approaches in Verification and Control

Posted: 8th September 2015

Fully Funded Doctoral Studentship

New Machine Learning Approaches in Verification and Control

Supervisors: Daniel Kroening & Alessandro Abate

Start Date: January 2016

The Systems Verification Research Group is offering one fully-funded D.Phil studentship in Oxford University's Department of Computer Science. The studentship will cover fees at home/EU rates. There will also be provision for some travel funds. The studentships will be funded for three years and will start as early as January 2016.

We are interested in the convergence and integration of recent techniques from statistical and machine learning with successful approaches for the formal verification of reactive models. We are specifically focused in the development of innovative solutions for planning and control synthesis over models of dynamical systems, in particular of autonomous aerial robotics or of multi-agent compositions of ground vehicles. The project will investigate the verification and control of complex models in robotics, encompassing the presence of continuous physical components, as well as of discrete digital software and actuation: this naturally yields a cyber-physical modelling setup, which is challenging for verification and control tasks.

The convergence of learning and verification techniques is key in this project. In verification, the use of machine learning to guess simple linear program invariants is promising, but complex invariants, in particular for the CPS setup mentioned above, appear to be difficult for existing statistical learning techniques. Statistical approaches in model checking are promising in terms of scalability, but often lack providing stringent assertions that are required for safety verification tasks. On the other hand, key algorithmic ideas in verification such as efficient splitting and learning in conflict-driven clause learning and symbolic reasoning about sets have the potential to improve existing learning techniques. Further, we are interested in the integration of advanced, adaptive model learning techniques from data, with successful model-based approaches for verification, control and planning. For the verification and correct-by-design control of complex models that are relevant in the discussed robotics applications, we target the in-the-loop coupling of such diverse perspectives, which leads to specific scalability and computational requirements.

We invite proposals for doctoral study in either of the above-mentioned topics (learning vs verification) that are relevant to the project. Suitable candidates need to have a strong background in mathematics. We further appreciate expertise in the domain of planning and control of robotic vehicles, with a keen interest to broaden towards verification.

Prospective applicants should include a clear statement of how they plan to contribute to the above goals with their expertise and interests. Candidates must also have good writing, communication, presentation, and organisation skills.

Applicants must in addition satisfy the entry requirements for studying for a doctorate at Oxford:

There is no deadline for applying. We will continue to process applications until a suitable candidate is found. Candidates are therefore recommended to apply as soon as possible and to inform Julie.sheppard@cs.ox.ac.uk when they have done so.

Please also email if you have any questions about the application process.

Please quote CS-DK-AA-Stud16 in the studentship reference box