About the project
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:
The School of Electronics and Computer Science is committed to promoting equality, diversity inclusivity as demonstrated by our Athena SWAN award. We welcome all applicants regardless of their gender, ethnicity, disability, sexual orientation or age, and will give full consideration to applicants seeking flexible working patterns and those who have taken a career break. The University has a generous maternity policy, onsite childcare facilities, and offers a range of benefits to help ensure employees’ well-being and work-life balance. The University of Southampton is committed to sustainability and has been awarded the Platinum EcoAward.
