Role
You will work on the synthesis of novel refinement propositions and proofs obtained via state-of-the-art theorem provers and model-checkers. There will be a need to develop novel synthesis algorithms that can scale. There will be a need to fine-tune foundational models using the produced datasets and to evaluate their performance on benchmark problems. Novel reasoning techniques integrating LLMs and state-of-the-art provers will be developed, and there will be a need to formally justify their soundness. You will liaise with academics in the project and participate in the writing of papers.
You will have the opportunity to further extend and develop your knowledge of formal methods, software engineering, and artificial intelligence whilst within the role.
Skills, Experience & Qualification needed (these can be taken from the person specification)
You will have a PhD in formal methods, and experience on modelling and proof of algebraic refinement propositions using CSP, and their mechanisation in FDR. Experience with use of theorem proving using Isabelle, and usage of Large Language Models (LLMs), including fine-tuning, is highly desirable. You will have experience with an object-oriented and or functional programming language.
Interview date: To be confirmed