Computers play a vital role in controlling modern cars, aeroplanes and trains. For instance, many airports now have driverless trains to take passengers from one terminal to another. We study the theory and practice of hardware and software verification to ensure that such safety-critical systems perform correctly.

Typically, our methods allow users to encode a specification of the desired behaviour in a high-level logical language. Users can formally prove that the computer code matches its specification by using computer verification tools. Users often desire to be able to express many different notions such as time, location, belief, knowledge, trust and even intentions. For example, a user might want to ensure that a driverless train’s doors remain closed until the train is stationary. But the more expressive the logical languages, the more difficult it is to find proofs.

Our research aims to design the logical language that is appropriate for a user's task, find proof-methods for this language and build prototypes to show that our methods are effective. Ultimately, we seek to turn our prototypes into efficient tools that can be used in industrial applications. 

Explore our available student research projects below and if you’d like to discuss opportunities for collaboration or funding, please email us.