[School of Engineering PhD Scholarships] Verified and reproducible execution of AI models

About the project

About the Project The existing software infrastructure for the training, testing, and deployment of AI models such as neural networks has an inherent weakness: the same model may produce different outputs when executed on different machines. While these discrepancies might be acceptable for general-purpose applications, they constitute a serious obstacle towards the safety of AI-enabled systems in aerospace and related safety-critical industries. This is because, any attempt at assuring the correctness of an AI model during development (via testing of formal verification) does not necessarily translate to a correctness guarantee on the deployment machine [1]. This project aims at addressing the challenge in two stages. First, we need a non-ambiguous formal specification of the behaviour of an AI model at the implementation level. The formal specification must describe the full computational graph that is executed during training and inference, while guaranteeing portability and reproducibility across machines. The work will rely on software verification and synthesis tools (e.g. ESBMC, Why3), while interfacing with existing neural network standards (e.g. ONNX, VNN-LIB). Second, we need automated assurance methods for AI models written in the above specification. These must be compatible with emerging aerospace standards like ED-324/ARP 6983 and enable us to certify the model correctness with respect to given engineering requirements. To this end, the research will focus on static analysis and formal verification techniques that take into account numerical accuracy and other software implementation details. The potential outcomes of the project are as follows: - Contributions to and improvement of the safety-related ONNX profile (SONNX), an emerging international standard for the specification of safety-critical computational graphs and neural networks [2], in the form of finite-precision operator specifications, automated numerical error propagation tools, and reproducibility testers. - Contributions to the VNN-COMP competition and the broader neural network verification community [3], in the form of bit-precise verification tools, witness checkers, equivalence checkers, and benchmarks for floating-point and quantised numerical types. - A strengthening of existing ties with the broader SONNX community, which includes companies like Airbus and Thales, with opportunities for further collaborations in the aerospace and autonomous robotics space. - Top-tier publications in relevant conference venues such as CAV, TACAS, AAAI, ICSE and journals such as TOSEM, ASE, RAS. In terms of support and training, the PhD candidate will be part of the Systems and Software Security group in the Computer Science department. Here, they will have access to state-of-the-art software verification tools, hands-on-training in neural network verification, and opportunity to learn from a security-oriented community of researchers. Further advice on the needs of the aerospace industry, formal verification methods, and numerical analysis will be provided by the external collaborators. In addition to the standard departmental training, the student will also be encouraged to attend relevant workshops, summer schools and conferences in the formal methods space. The supervisory process will involve regular weekly meetings which will cover research progress, technical advice, career development, and presentation and writing skills. [1] Cordeiro, et al. “Neural network verification is a programming language challenge”. ESOP. 2025. [2] https://github.com/ericjenn/working-groups/tree/ericjenn-srpwg-wg1/safety-related-profile [3] https://vnn-comp.github.io/ This project is expected to start in September 2027. Before you apply: We strongly recommend that you contact the supervisors for this project before you apply. How to apply: To be considered for this project you must complete a formal application through our online application portal. If you already have an applicant account this link will directly open an application for PhD School of Engineering Scholarships . If you don’t already have an applicant account, please follow the instructions here. . When applying, please specify the full title and supervisor/s of the project, details of your previous study, and names and contact details of two referees. You must also upload a Supporting Statement describing the motivation to apply to the project, your CV and transcripts of awarded and in-progress university qualifications . Please note late or incomplete applications will not be considered. Equality, diversity and inclusion are fundamental to the success of The University of Manchester and central to all our activities. A diverse research community strengthens creativity, productivity and quality, while increasing the societal and economic impact of our work. We welcome applicants from all career paths, backgrounds and sections of the community, regardless of age, disability, ethnicity, gender, gender expression, sexual orientation or transgender status. We welcome applications from candidates returning to study after a career break or experience in other roles. Flexible study arrangements may be available, including part-time study at 50%, 60% or 80%, subject to the requirements of the project and funder. Eligibility : The standard academic entry requirement for this PhD is an upper second-class (2:1) honours degree in a discipline directly relevant to the PhD Computer Science (or international equivalent) OR any upper-second class (2:1) honours degree and a Master’s degree at merit in a discipline directly relevant to the PhD Computer Science (or international equivalent). This project will remain open until filled. If your application is submitted by 1 st November 2026, you can expect a decision by 18 th December 2026. If your application is submitted by 15 th January 2027, you can expect a decision by 30 th March 2027. Self or externally funded students can also be considered for this project. FSESoE

Research areas