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
The development of the Hume box calculus (with Greg Michaelson)
A mechanisation of TLA* in Isabelle/HOL (with Stephan Merz), which I have used to reason about Hume programs and transformations.
A formalisation and mechanisation of Hume resource reasoning using Isabelle/HOL (with Hans-Wolfgang Loidl)
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:
The Tinker tool for PSGraphs, with support for the Isabelle, ProofPower and Rodin theorem provers
The Tacny tool, which adds support for user-defined "tactics" in the Dafny program verifier
The DARe tool which removes auxiliary annotations of Dafny programs
The CORE system for separation logic
Formalisation of TLA* and Hume resource reasoning in Isabelle/HOL
I have developed a model checker for HW-Hume using SPIN and TLA+
Funding
Principal Investigator on UiO "studiekvalitetsmidler" project: Delautomatisert, dynamisk og gjenbrukbart labsystem for praktisk erfaring m grunnleggende konsepter innenfor informasjonssikkerhet (Summer 2023)
Principal Investigator on UiO "studiekvalitetsmidler" project: VM/skybasert miljø for workshop-oppgaver i informasjonssikkerhet (Summer 2022)
SICSA Early Career Industrial Fellowship to work with D-RisQ (Oct 2015 - Jun 2017)
Co-Investigator on the EPSRC funded platform grant: The Integration and Interaction of Multiple Mathematical Reasoning Processes [webpage] (EP/N014758/1: 1 Nov 2015 - 31 Oct 2019)
Co-Investigator on QAA Student Enhancement project: Transition from passive learner to critical evaluator through peer-testing of programming artifacts (Manuel Maarek (PI); Jan 2017 - May 2017)
Principal Investigator on EPSRC grant: DTacs - Program Verifier Tactics : Reducing the Development Time for Program Verifiers with re-usable Verification Strategies (EP/M018407/1) [link] (Jun 2015 - Nov 2016)
Principal Investigator on QAA Student Enhancement project: Transition of automated feedback and marking into student’s learning environment (Jan 2016 - Aug 2016)
Co-Investigator on the EPSRC funded platform grant: The Integration and Interaction of Multiple Mathematical Reasoning Processes [webpage] (EP/J001058: 1 Aug 2011 - 31 Oct 2015)
Principal Investigator on Heriot-Watt's EPSRC Impact Acceleration Account project: A flexible and adaptable proof tool for verification of control systems in evolving markets (with D-RisQ ; Nov. 2014 - Sept. 2015)
Co-Investigator on QAA Student Enhancement project to implement technology enhanced learning principles in Computer Science courses with Verena Rieser (Jan 2016 - Jul 2015)
Co-Investigator on the EPSRC funded project AI4FM: using AI to aid automation of proof search in Formal Methods
James Watt Scholarship from Heriot-Watt to support my PhD.