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 Jeremy Dawson »

Research Fellow

Professor Rajeev Gore »


Dr Ekaterina Lebedeva »

University Lecturer

Dr Dirk Pattinson »

Assoc Director (Research)

Dr Badri Ravisankar »

Research Fellow

Professor John Slaney »



Daniel Alarcon

Mr Daniel Alarcon »

PhD Student

Joshua Bax

Mr Joshua Bax »


Mr Elliot Catt »


Mr Sina Eghbal »

Masters Student

Hendra Gunadi

Mr Hendra Gunadi »

PhD student

Mr Minjian Liu »


Ms Caitlin McGregor »

PhD Student

Jingyu Shao »

PhD Student

Mukesh Tiwari »

PhD Student

Florence Verity

Ms Florrie Verity »


Dr Qiongkai Xu »

Postdoctoral Fellow

Mr Yifei Zhang »

Masters Student

Mr Rui Zhang »

Masters Student


Dr Peter Baumgartner »

Honorary Assoc Prof

Dr Michael Norrish »

Visiting Fellow


Prof Marcus Kracht »

Campus Visitor

Mr Tobias Wangberg »

Occupational Trainee


Journal Articles

  1. Baumgartner, P., Armando, A., Dowek, G., (2010). Preface. Journal of Automated Reasoning.
  2. Baumgartner, P., Furbach, U., Pelzer, B., (2010). The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation.. Journal of Logic and Computation20(1):77–109.
  3. Baumgartner, P., Thorstensen, E., (2010). Instance Based Methods-A Brief Overview*. Kuenstliche Intelligenz`24(1):35–42.
  4. Baumgartner, P., Waldmann, U., (2010). A Combined Superposition and Model Evolution Calculus.Journal of Automated ReasoningOnline:1–37.
  5. Kramer, S., Gore, R., Okamoto, E., (2010). Formal definitions and complexity results for trust relations and trust domains fit for TTPs, the Web of Trust, PKIs, and ID-Based Cryptography. SIGACT News41(1).
  6. Tiu, A., Gore, R., Dawson, J., (2010). A Proof Theoretic Analysis of Intruder Theaories. Logical Methods in Computer Science6(3):1–37.
  7. Tiu, A., Millar, D., (2010). Proof search specifications of bisimulation and modal logics for the n-calculus.ACM Transactions on Computational Logic11(2):37

Conference Papers

  1. Bauer, A., Botea, V., Brown, M., Gray, M., Harabor, D., Slaney, J.K., (2010). An Integrated Modelling, Debugging, and Visualization Environment for G12. In D. Cohen (ed.), International Conference on Principles and Practice of Constraint Programming 2010, pp. 15, St Andrews Scotland.
  2. Gore, R., Dawson, J., (2010). Generic Methods for formalising sequent Calculi Applied to provability logic. In Christian G. Ferm (ed.), 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 263–277, Yogyakarta, Indonesia.
  3. Gore, R., Kupke, C., Pattinson, D., (2010). optimal Tableau Algorithms for Coalgerbraic Logics. In J. Esparza and R Majumdar (eds.), International Conference on TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS 2010, Paphos Cyprus.
  4. Gore, R., Kupke, C., Pattinson, D., Schroder, L., (2010). Global Caching for Coalgebraic Description Logics. In International Joint Conference on Automated Reasoning 2010, pp. 15, Edinburgh Scotland.
  5. Gore, R., Widmann, F., (2010). optimal and Cut-Free Tableaux for propositional dynamic logic with converse. In International Joint Conference on Automated Reasoning 2010, Edinburgh Scotland.
  6. Tiu, A., Dawson, J., (2010). Automating Open Bisimulation Checking for the Spi Calculus. In IEEE Computer Security Foundations Symposium 2010, pp. 15, Edinburgh Scotland.


Updated:  8 September 2015/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing