 | Jacques Fleuriot | My main field of research lies in AI Modelling, which spans areas such as interactive theorem proving, formal verification, process modelling, and machine learning and Explainable AI techniques applied to healthcare and other complex domains. |
 | Ricardo Contreras | Monitoring of dynamic process compositions and data processing with focus on older adults. |
 | Nuša Farič | Nuša has interests in psychology, health psychology, AI, femtech, women’s health, health content on Wikipedia and innovative health solutions. She studied at the University of Glasgow (BSc Hons Psychology), UCL (MSc Health Psychology), and PhD (Health Psychology and Informatics for the UCL Institute of Health Informatics). |
 | Filip Smola | Interactive theorem proving and formal verification, with application to automatic differentiation, category theory and process calculi. |
 | Jorge Gaete Villegas | Explainable AI for healthcare. |
 | James Vaughan | Applications of ML and Network Theory in Automated Theorem Proving; Business Process Modelling and IoT. |
 | Lauren DeLong | Artificial Intelligence and medicine/healthcare. |
 | Zonglin Ji | Artificial Intelligence for ICU care and predictions |
 | Richard Schmoetten | Formalising Haag-Kastler Nets in Higher-order Logic. |
 | Matt Whelan | My main interests are in AI applications in psychiatry, with a particular focus on predicting mental/cognitive health outcomes from sleep and activity patterns. |
 | Alex Hyman | Interested in exploring the world of Isabelle and formally verifying mathematics |
AIML Associates/Interns
 | Petros Papapanagiotou | AI for collaborative workflow management. This includes formal verification, process modelling, analysis and optimisation, IoT, event-based and distributed systems, and social machines. |
 | Mark Chevallier | Theorem proving, formal verification for AI, LLM for finance. |
 | Jake Palmer | Theorem proving, voting algorithms, data and process mining. |
 | Jiawei Zheng | Uncertainty in complex event processing, process mining, and conformance checking. |
Recent AIML Alumni
Konstantin Georgiev (PhD, 2025) | Harnessing Routine Data and Healthcare Contacts to Predict Risk and Treatment Requirements in Older People |
Filip Smola (PhD, 2025) | A Formalised Approach to the Composition ofProcesses over Linear Resources |
Paola Galdi (Research Associate, 2025) | Machine learning and statistical modelling for biomedical data, multimodal data integration, network-based modelling. |
Guillermo Moreno (Research Associate, 2025) | Interdisciplinary research in AI, ML, and network science applied to various areas, such as politics, health, biology, robotics, etc. |
Jiawei Zheng (PhD, 2024) | Process-aware Pattern Recognition and Deviation Detection Under Uncertainty |
Lune De Ferrari (Senior Research Associate, 2025) | Applied ML (broad and deep) and statistics for NLP and protein function prediction. Interested in DevOps, agile practices and software development coordination. |
Ramon Fernández Mir (PhD, 2024) | Verified transformations for convex programming |
Jorge Gaete Villegas (PhD, 2024) | Modelling and predicting medical outcomes for intensive care patients via network mechanisms and machine learning |
Jake Palmer (PhD, 2023) | Rigorous treatment of Meek’s method for single transferable vote with formal proofs of key properties |
Mark Chevallier (PhD, 2023) | Verification using formalised mathematics and theorem proving of reinforcement and deep learning |
Simon U (BSc, 2023) | Deep Learning for ADL recognition |
Matt Whyte (MSc, 2023) | Generating efficient PyTorch code from formal specification (Outstanding Informatics MSc in Artificial Intelligence thesis 2023) |
Gareth Dawson (BSc, 2023) | A front-end graphical user interface for the Proter Simulator |
Leo Kravtchin (MInf, 2023) | Detecting Long-Term Deviation and External Factors Correlations in Activities of Daily Living Based on Sensor Data |
Imogen Morris (PhD, 2022) | Mechanising Euler’s use of infinitesimals in the proof of the Basel problem |
Scott O’Donoghue (MSc, 2022) | Applying Machine Learning and Interpretable Techniques to Persistent Critical Illness |
Carlin Mackenzie (MInf, 2022) | Developing an online proof archive for formalized mathematics |
Dawson Silkenat (BSc, 2022) | Formalisation of Lagrangian Mechanics in Isabelle/HOL |
Lars Werne (BSc, 2022) | Formalisation of Newtonian Physics in Isabelle/HOL |
Martin Lewis (BSc, 2022) | Web development for business process simulation |
Michal Sadowski (BSc, 2022) | Workflow execution and management |
Dimitris Christodoulou (MInf, 2022) | Activity tracking and localisation using Wi-Fi data |
Michal Baczun (MInf, 2022) | Business process simulation |
Petros Papapanagiotou (Chancellor’s Fellow, 2022) | AI for collaborative workflow management. This includes formal verification, process modelling, analysis and optimisation, IoT, event-based and distributed systems, and social machines. |
Callum Abbot (MSc, 2021) | To Drain or Not to Drain? A Causal Investigation into the Efficacy of Subdural Drains in Preventing CSDH Recurrence (MSc in Data Science thesis prize) |
Yefei Chen (MSc, 2021) | Designing checklists generated from process models |
Qi Chen (MSc, 2021) | Delay visualization in process timelines |
Mathis Gerdes (MSc, 2021) | Investigating causality in axiomatic Minkowski spacetime using Isabelle/HOL |
Cyan Hou (MSc, 2021) | A web framework for negotiation strategies in multi-agent meeting scheduling |
Shilin Li (MSc, 2021) | Incorporating cultural preferences in meeting scheduling applications |
Alice Johansen (BSc, 2021) | Formalisation of proofs from Euler’s Foundations of Differential Calculus using Nonstandard Analysis (I) |
Richard Stansfield (BSc, 2021) | Formalisation of proofs from Euler’s Foundations of Differential Calculus using Nonstandard Analysis (II) |
Richard Schmoetten (MSc, 2020) | Axiomatic Minkowski Spacetime in Isabelle/HOL (MSc in Informatics thesis prize) |
Colleen Charlton (MSc, 2020) | Interpretable classifiers for brain tumour prediction (Outstanding Informatics MSc thesis 2020) |
Anita Klementiev (MSc, 2020) | Process mining techniques for modelling healthcare patients’ paths in the ICU/CCU |
Yannan Huang (MSc, 2020) | Process analytics for the training of future doctors |
Demetris Louca (MSc, 2020) | Analysis of process miners |
Yaqing Jiang (PhD, 2019) | Machine Learning for Inductive Theorem Proving |
Callum Biggs-O’May (MSc, 2019) | Investigating Brain Cancer Survival with Machine Learning (Outstanding Informatics MSc thesis 2019) |
Kezhi (Bill) Chen (MSc, 2019) | Delay Analysis in Manufacturing Process |
Ka Wing Pang (MSc, 2019) | Exploring Streams with Isabelle/HOL |
Jessika Rockel (MSc, 2019) | Exploring Euler’s Foundations of Differential Calculus in Isabelle/HOL using Nonstandard Analysis: Logarithms (Outstanding Informatics MSc thesis 2019) |
Simon Thorogood (MSc, 2019) | Predicting Transplant and Patient Survival Following Liver Transplantation using Machine Learning (MSc in Data Science thesis prize 2019) |
Zuzana Frankovska (BSc in Computer Science and Mathematics, 2019) | Exploring Euler’s Foundations of Differential Calculus in Isabelle/HOL using Nonstandard Analysis: Geometric Series and Arcsine |
Filip Smola (Summer Intern, 2019) | DigiFlow: Digitizing Industrial Workflow, Monitoring and Optimization |
Kyriakos Katsamaktsis (MMath, 2018; Summer Intern, 2019) | Exploring Euler’s Notions of Orders of Infinity in Isabelle/HOL using nonstandard analysis (MMaths Project Prize 2018) |
Nigel Hussain (MSc, 2018) | Business Process Modelling of Care Pathways for HIV Patients |
James Vaughan (MSc, 2018) | Learning over Isabelle’s Dependency Graphs |
Hristo Saev (BSc, 2018) | Developing a Social, Open, Peer Review Web Platform |
Ruitao Yi (Summer Intern, 2018) | Formalization of the Backpropagation Algorithm |
Steven Obua (Senior Research Fellow, 2014-2017) | ProofPeer: Collaborative Theorem Proving |
Phil Scott (Research Fellow, 2014-2017) | ProofPeer: Collaborative Theorem Proving |
Imogen Morris (BSc, 2017) | An Axiomatic Formalisation of Trigonometric Functions in Isabelle (BSc Maths Project Prize 2017) |
Jake Palmer (MSc, 2017) | A Mechanized Investigation of an Axiomatic System for Minkowski Spacetime |
Eirini Papakosta (MSc, 2017) | An Interactive, Web-based Platform for Pulmonary Rehabilitation |
Lie (Jessie) Ma (MSc, 2017) | An Interactive, Web-based Platform for Pulmonary Rehabilitation |
Daniel Raggi (Research Assistant, 2017) | Entailment Graphs in Isabelle/HOL |
Alisa Dewanti (MSc, 2016) | Developing workflow-based guidelines for burns care in Scotland |
Vanessa Hanschke (MSc, 2016) | A Social Machine for the Heart Manual Programme |
Sebastian Schulze (BSc, 2016; Summer Intern 2016) | Evolving Neural Networks for Natural Deduction Proofs |