PhD project: Verification of Neuro-Cyber-Physical Systems
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. Finally, 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 (https://github.com/vehicle-lang/vehicle) that provides a functional, domain-specific language for specifying, training, and verifying neural components. Depending on individual skills and interests, this PhD project has a scope for a student interested in either formal logic (quantitative, differential, linear logic), types & programming languages (functional DSLs, dependent types), or theorem proving and verification (solvers and provers, including interactive theorem provers such as Rocq or LEAN and neural network verifiers). The applicant is expected to have an MSc degree or equivalent, and a strong background in at least one of the above three broad areas of research. Knowledge of, and interest in, machine learning is a bonus.
This Scholarship fully covers all PhD fees and a PhD stipend for 4 years. There are no nationality requirements and restrictions. Please address all enquiries to E.Komendantskaya@soton.ac.uk
- Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.2