Mechanically Checking the Semantics of Hybrid Event-B at The University of Manchester

These days, the world is increasingly being populated with systems that interact directly with the physical world. Of course such systems have existed for a long time in niche safety-critical areas, eg. avionics, train control, nuclear plant shutdown, etc. Now the physical world is described using continuous mathematics, while the systems in contact with it are digital, being described using discrete mathematics. These two spheres don't mix terribly well, and the interface has typically been handled by ad hoc means. The hybrid and cyberphysical systems that are increasingly seen today are hard to analyse, and one way of approaching their design is top-down, where their properties are controlled from the outset and built up incrementally. The Event-B formalism is a discrete top-down formal development methodology which has become popular in the discrete domain, and Hybrid Event-B has been designed to extend it into the continuous domain. The aim of this project is to build a model of the semantics of Hybrid Event-B in a meta theorem prover like Isabelle/HoL or CoQ, and to demonstrate its soundness and the soundness of the Hybrid Event-B Proof Obligations.

Eligibility

Applicants should have, or expect to achieve, at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering related discipline.

Funding

This is a 3.5-year PhD. Excellent candidates will be nominated for competence-based funding.

Self funded students are welcome to apply.

The start date is October 2026.

We recommend that you apply early as the advert may be removed once the position has been filled.

Before you apply

We strongly recommend that you contact the supervisors for this project before you apply. Please include details of your current level of study, academic background and any relevant experience and include a paragraph about your motivation to study this PhD project.

How to apply

Apply online through our website: https://uom.link/pgr-apply-2425

When applying, you’ll need to specify the full name of this project, the name of your supervisor, if you already having funding or if you wish to be considered for available funding through the university, details of your previous study, and names and contact details of two referees.

Your application will not be processed without all of the required documents submitted at the time of application, and we cannot accept responsibility for late or missed deadlines. Incomplete applications will not be considered.

After you have applied you will be asked to upload the following supporting documents:

• Final Transcript and certificates of all awarded university level qualifications
• Interim Transcript of any university level qualifications in progress
• CV
• Supporting statement: A one or two page statement outlining your motivation to pursue postgraduate research and why you want to undertake postgraduate research at Manchester, any relevant research or work experience, the key findings of your previous research experience, and techniques and skills you’ve developed. (This is mandatory for all applicants and the application will be put on hold without it).
• Contact details for two referees (please make sure that the contact email you provide is an official university/work email address as we may need to verify the reference)
• English Language certificate (if applicable)

If you have any questions about making an application, please contact our admissions team by emailing FSE.doctoralacademy.admissions@manchester.ac.uk.

Equality, diversity and inclusion is fundamental to the success of The University of Manchester, and is at the heart of all of our activities. We know that diversity strengthens our research community, leading to enhanced research creativity, productivity and quality, and societal and economic impact.

We actively encourage applicants from diverse career paths and backgrounds and from all sections of the community, regardless of age, disability, ethnicity, gender, gender expression, sexual orientation and transgender status.

We also support applications from those returning from a career break or other roles. We consider offering flexible study arrangements (including part-time: 50%, 60% or 80%, depending on the project/funder).

_{uom_cs_theory_foundations}