Research
My key areas of interest are Formal Methods and Functional Languages.
In particular my research focusses on the development and use of the
Unifying Theories of Programming
(UTP) paradigm.
Application areas include:
clinical pathways;
medical device software; and spacecraft operating systems.
Current research explorations include:
- UTP theories of shared variable concurrency, including:
-
Developing a fully composition and "local" denotational semantics in UTP
for shared-variable concurrency, as a baseline for other work below that goes up the abstraction ladder.
-
Exploring approaches for UTP semantics for rely/guarantee reasoning,
Owicki-Gires, and seperation logic
(in collaboration with
Jim Woodcock
)
-
Using UTP results on shared-variable concurrency
to give a semantics to Process Modelling Language (PML),
in collaboration with John Noll and Anila Mjeda.
- Implementing a variety of proof asisstance tools
for UTP, written in Haskell:
Theorem Proving Assistant for UTP
;
UTP Calculator
;
Equational Reasoning Support
.
I am actively involved in
Lero: the Irish Software Research Centre
.
Current Projects
RTEMS-SMP
Formal verification of multicore real-time scheduling.
Funded by ESA (2yrs, started Feb 2019).
FMHIDA
Investigating formal techniques for medical device software development.
Funded by SFI through Lero, Hub A (Ongoing, 2016-2020)
Past Activities
I was involved in the following projects:
-
Acted as a formal-methods expert for a ESA-funded
activity investigating the qualification of seperation kernels for integrated modular avionincs
(FMEIMAKQP)
-
Led a ESA-funded
activity on O/S kernel formal verification (MTOBSE, Tasks 3 & 4).
-
Formalising Interfaces between Software and Hardware
funded by SFI
-
Unifying Synchronous Systems
funded by SFI
- Formal models of NAND Flash memory
based on the ONFI standard, for use
in verified file-stores for mission-critical data storage
applications.
Part of a case-study for
GC6: Dependable Systems Evolution .
- Extensions to the Unifying Theories of Programming (UTP) to cater
for synchronously clocked hardware systems.
- Formal aspects of functional languages, with emphasis on I/O
behaviour
- Formal Semantics for the Handel-C
hardware programming language (in collaboration with
Jim Woodcock ).
- Synchronous Circus
(also in collaboration with
Jim Woodcock ).
- Adding unbounded demonic and angelic non-determinism to
deterministic semantic theories (in collaboration with Joseph Morris ).
- The "Irish School of VDM", a functional
dialect of VDM developed here at TCD.
- Formal Models of External I/O for Pure Lazy Functional Languages
(funded by Enterprise Ireland SC-2002-283).
- Enterprise Ireland funded
Formal Aspects of CORBA project
- EU funded HCM project "DeStijl".
