Verification of Neuro-Cyber-Physical Systems

About the Project

Supervisory Team: Ekaterina Komendantskaya

Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers.

Symbolic models of the “cyber” and “physical” behaviour of the system must be constructed and verified in interactive theorem provers, often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics. The results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model.

This project will develop a compositional methodology for constructing such proofs in the Vehicle framework that provides a functional, domain-specific language for specifying, training, and verifying neural components of cyber-physical systems. Depending on your skills and interests, the project is well‑suited for students interested in:

• formal logic (quantitative, differential, linear logic)
• types & programming languages (functional DSLs, dependent types)
• theorem proving and verification (solvers and provers, including interactive theorem provers such as Rocq or LEAN and neural network verifiers)

You'll be a part of a large network of international collaborators, and you'll attend relevant meetings, seminars and conferences.

Learn more about this research:

• Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs

Entry requirements

You must have a UK 2:1 honours degree, or its international equivalent, in one of the following:

• mathematics
• engineering
• computer science

Relevant experience in logic, functional programming languages, or formal verification is essential. Knowledge of, and interest in, machine learning is desirable.

Fees and funding

This project is fully funded through an Industrial CASE (Cooperative Awards in Science and Technology) studentship.

Tuition fees will be paid, and you'll receive an annual stipend for up to 4 years.

How to apply

Apply now

You need to:

• choose programme type (Research), 2026/27, Faculty of Engineering and Physical Sciences
• select Full time or Part time
• search for programme PhD Computer Science (7089)
• add name of the supervisor in section 2 of the application

Applications should include:

• research proposal
• your CV (resumé)
• 2 academic references
• degree transcripts and certificates to date
• English language qualification (if applicable)