FORMAL MODELLING of process workflows (and more)
Work on the development and application of the WorkflowFM framework is ongoing. This encompasses areas such as healthcare and manufacturing (e.g. as part of the Digiflow project).
Past and ongoing projects include (amongst others) the modelling of integrated care pathways (ICPs) for HIV (in association with NHS Lothian and NHS Greater Glasgow & Clyde), developing rigorous models for the treatment of burns (in collaboration with the Glasgow Royal Infirmary) and modelling the processes underlying patient transfers in hospitals (in collaboration with St Mary’s Hospital, London). More information is available on WorkflowFM.org and WorkflowFM.com
Our domain- agnostic approach and technology is based on a correct-by-construction approach. It enables the development of high-level process models and workflows that can be faithfully deployed as software through automatic code-generation. The workflows can be integrated with data, e.g. coming from IoT devices, and monitored through our custom-built dashboard.
DIGIFLOW
Digitizing Industrial Workflow, Monitoring and Optimization
The WorkflowFM team (Smola, Vaughan, Papapanagiotou and Fleuriot) is working on the transfer of its formal-methods based technology to a real-world context involving the modelling and deployment of industrial workflows tracking shopfloor assets and workforce.
Funder: EIT Digital
Partners: FBK CREATE-NET, Reply, ThinkINside.
Total Funding: 500K EUR (2018) + 550K EUR (2019)
AI4T: AI FOR TRANSPLANTATION
Predictive AI modelling for liver transplantation
Project on predicting graft and patient survival following liver transplantation is currently underway. We’re working with a large dataset obtained from the National Health Service Blood & Transplant (NHSBT).
This work has so far resulted in a Poster of Distinction Prize at the Association of Surgeons in Training International Surgical Conference 2019 and in a best dissertation prize for an MSc in Data Science (2019) for Simon Thorogood’s work on “Predicting transplant and patient survival following liver transplantation using machine learning”.
Collaborators: Oxford University NHS Trusts.
AI-BASED SURVIVAL ANALYSIS
modelling brain tumour survival using machine learning
This project investigates survival of patients with brain cancer using a specially curated dataset that includes genetic tests, tumour characteristics, demographic, clinical and treatment information .
This work has so far resulted in a MSc thesis titled “Investigating Brain Cancer Survival with Machine Learning” for Callum Biggs O’May. In this thesis, one of the oustanding MSc projects of 2019, machine learning techniques are used to interrogate the clinical consensus on how the above-mentioned factors influence one another and which are important for survival.
Collaborator: Paul Brennan, Senior Clinical Lecturer and Honorary Consultant Neurosurgeon at the University of Edinburgh and NHS Lothian.
RECONSTRUCTING EULER
Mechanizing Euler’s infinitesimal and infinite reasonning in Isabelle/HOL
Several projects on the formal reconstruction of Euler’s proofs involving infinitesimal and infinite reasoning using Nonstandard Analysis are currently underway in the theorem prover Isabelle.
Sources include Euler‘s famous Introductio in analysin infinitorum (Introduction to the Analysis of the Infinite), first published in 1748, and his Institutiones calculi differentialis (Foundations of Differential Calculus), first published in 1752.
Aside from an ongoing PhD research project involving Imogen Morris, this work has led to two undergraduate final year projects, including a winner of the dissertation prize in Mathematics by Kyriakos Katsamaktsis for his work on Euler’s notions of orders of Infinity in Isabelle/HOL, and one outstanding MSc project (2019) by Jessika Rockel for her work on “Exploring Euler’s Foundations of Differential Calculus in Isabelle/HOLusing Nonstandard Analysis”.
AI FOR THEOREM PROVING
intelligent theorem proving
We are working on predictive modelling and new visualisation techniques to support work with proof assistants. These include intelligent exploration of proof libraries, proof analytics and predictive help during proof. This work incorporates and extends the technology from the ProofPeer project on collaborative theorem proving.