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.
Student research projects
- Baumgartner, P., Armando, A., Dowek, G., (2010). Preface. Journal of Automated Reasoning.
- Baumgartner, P., Furbach, U., Pelzer, B., (2010). The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation.. Journal of Logic and Computation, 20(1):77–109.
- Baumgartner, P., Thorstensen, E., (2010). Instance Based Methods-A Brief Overview*. Kuenstliche Intelligenz`, 24(1):35–42.
- Baumgartner, P., Waldmann, U., (2010). A Combined Superposition and Model Evolution Calculus.Journal of Automated Reasoning, Online:1–37.
- 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 News, 41(1).
- Tiu, A., Gore, R., Dawson, J., (2010). A Proof Theoretic Analysis of Intruder Theaories. Logical Methods in Computer Science, 6(3):1–37.
- Tiu, A., Millar, D., (2010). Proof search specifications of bisimulation and modal logics for the n-calculus.ACM Transactions on Computational Logic, 11(2):37
- 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.
- 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.
- 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.
- 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.
- 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.
- Tiu, A., Dawson, J., (2010). Automating Open Bisimulation Checking for the Spi Calculus. In IEEE Computer Security Foundations Symposium 2010, pp. 15, Edinburgh Scotland.