Skip to content

Research Associate

Computer Science
Based at
University of York - Heslington Campus
Hours of work
Contract status
Fixed term
31,604 a year
Apply by

Role Description

Applications are invited for a Research Associate to carry out research on application of formal verification technology to safety assurance of autonomous robots. This position will be funded by the EPSRC for three years in the context of the recently awarded CyPhyAssure project.

You will assist in the development of a computerised platform for arguing the safety of autonomous robots by application of multi-model based assurance cases. We will build this platform within the Isabelle/HOL proof assistant, and utilise the Structured Assurance Case Metamodel (SACM). The platform, as conceived, will support formal modelling of individual modular components of a robot and its environment, the combination of these models to describe the overall system’s behaviour, the description of formal requirements of the overall system, and decomposition and apportionment of these requirements to the constituent models.

The work will involve mechanisation of formal relational semantics in Isabelle/HOL for a variety of modelling languages (such as Simulink) utilising Hoare and He’s Unifying Theories of Programming (UTP), development of proof techniques, integration of the semantic models in a mechanised assurance case, and development of refinement techniques for constructing safety arguments. We will apply our technology to a number of assurance demonstrators provided by our industrial partners, construct a repository of examples based on this, and create guidelines and methods to support application of the technology.

Your main tasks will be to:

  • *assist in creating the assurance platform in Isabelle/HOL;
  • *integrate proof and verification techniques to provide evidence for assurance cases;
  • *support the development of the demonstrator repository using our technology;
  • *creation of appropriate documentation and guidelines in the use of the technology.

You will liaise with academic and the industrial partners and participate in the writing of research papers. You will have a PhD in the area of formal methods, experience in modelling and formal refinement, and understanding of hybrid and/or probabilistic systems. You will have substantial experience in the application of the Isabelle/HOL theorem prover. Experience in the areas of assurance cases, safety processes, and robotics are all highly desirable.

Informal enquiries can be made in the first instance to Dr Simon Foster (

The University is committed to promoting a diverse and inclusive community  – a place where we can all be ourselves and succeed on merit. We offer a range of family friendly, inclusive employment policies, flexible working arrangements, staff engagement forums, campus facilities and services to support staff from different backgrounds.

      Athena Swan Bronze               

A place where we can ALL be ourselves #EqualityatYork



Forgot password | Register

Why York?

York is one of the most successful universities in the UK.

With world-class activity across the spectrum from the physical sciences, life sciences, and social sciences to the humanities, we have been recognised as one of the top 100 universities in the world, gaining outstanding results in official assessments of our research and teaching.