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.

Academic staff

Dr Ranald Clouston »


Dr Jeremy Dawson »

Research Fellow

Professor Rajeev Gore »


Dr Ekaterina Lebedeva »

University Lecturer

Dr Dirk Pattinson »

Assoc Director (Research)

Professor John Slaney »


Dr Alwen Tiu »

Senior Lecturer


Daniel Alarcon

Mr Daniel Alarcon »

PhD Student

Mr Elliot Catt »

PhD Candidate

Hing Lun (Joseph) Chan

Mr Hing Lun (Joseph) Chan »

PhD Student

Ms Caitlin D'Abrera »

PhD Student

Mr Jim De Groot »

PhD Student

Mr Sina Eghbal »

Masters Student

Ian Shillito »

PhD Student

Mukesh Tiwari »

PhD Student

Florence Verity

Ms Florrie Verity »


Minchao Wu »

PhD Student


Dr Peter Baumgartner »

Honorary Assoc Prof

Dr Michael Norrish »

Visiting Fellow

Code Title Semester Offered in 20' Course convener
COMP1130 Programming as Problem Solving (Advanced) S1 18, 19, 20, 21 Professor Tony Hosking
COMP2620 Logic S1 18, 19, 20, 21 Professor John Slaney
COMP6262 Logic S1 18, 19, 20, 21 Professor John Slaney
MATH6203 Foundations of Mathematics S1 17, 18
COMP1600 Foundations of Computing S2 18, 19, 20, 21 Dr Dirk Pattinson
COMP6260 Foundations of Computing S2 18, 19, 20, 21 Dr Dirk Pattinson
COMP4630 Advanced Topics in Logic and Computation S2 17, 19 Professor Rajeev Gore
COMP8670 Advanced Topics in Logic and Computation S2 17 Professor Rajeev Gore

Updated:  1 November 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing