Research projects

Detlearsom - Detection by Learning Software Models

By combining methods from machine learning and formal verification, we plan to learn precise semantic models of software and devices which describe normal traffic patterns and logging behaviours. Then anomalous, potentially malicious behaviours stand out as being different to these learned behaviours. The eventual aim is to build an adaptive anomaly detection framework, to raise alarms to help manage and automatically configure application-level firewalls. More details on project webpage.

The Tacny project

The Tacny project is supported by EPSRC's first grant scheme. Here the goal is to develop and implement a notion of `verification patterns' for the Dafny program verifier. More information can be found on the project webpage.

PSGraph & Tinker

PSGraph is a graphical and hierarchical representation of proof strategies, which has been implemented as a tool called Tinker. This tool supports two theorem provers: Isabelle and ProofPower theorem provers. Details of the particular language and tool can be found on the project webpage. The development of the language started with the EPSRC funded AI4FM project (see project webpage), and has later been supported by an Impact Acceleration Account grant and a SICSA early career industrial fellowship. We have also investigating how Meta-Interpretive Learning can be used to learn proof strategies within PSGraph.

Reasoned modelling

The idea with the reasoning modelling paradigm, developed mainly with Andrew Ireland and Teresa Llano, is to lift user interaction and reasoning to the modelling level within so-called posit-and-prove formal methods. The goal of reasoning modelling is that the user focuses on high-level modelling choices, by hiding underlying and low-level proof details. Reasoning modelling critics abstracts proof failures into a suggested change to a formal model; refinement plans are high-level refinement patterns which can be used to guide proofs and proof failure patching; while design space exploration uses computational creativity and theory exploration to generate "correct" abstractions or adaptations of a given flawed specification.

Hume

My PhD work [link, PDF] was concerned with functional correctness and transformation of Hume programs using Lamport’s TLA logic and Isabelle/HOL. My MSc thesis [link, PDF] addressed model checking of a Hume subset called HW-Hume (hardware Hume) using the Spin model checker. I have also been employed on the EU-funded EmBounded project, where I addressed model checking of Hume, and resource verification of imperative programs using Hume. My key contributions here has been 

Functional verification in separation logic

I have previously worked for/with Andrew Ireland and Ewen Maclean on functional verification of properties in separation logic, employed on the EPSRC funded CORE project. A key contributions here has been participating in the development of the CORE system for functional verification of separation logic.

Tool development

I have led or been involving in the development of the following tools:

Funding