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)

Publications

?-Challenges

Past Activities

• 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".

Community

I am on the Editorial Board of Formal Aspects of Computing

I am currently on the programme committee of: TASE 2019.

I have have served on the following programme committees: IWFM, NFWM, FMICS, FM, IFL, TFP, UTP, ICTAC, ICFEM, SBMF, among others.

I was active in the Irish Formal Methods Special Interest Group IFMSIG), a programme committee member and former co-chair for IWFM and a maintainer of the IFMSIG mailing lists. I was also a member of the Irish Mathematical Society.

I also used to assist in organising the occaisional/annual Trinity Week Academic Symposium,

I was also a founder-member and director of the Skrabanek Foundation, named after the late Petr. Skrabanek of Trinity College, and dedicated, like his life, to the encouragement of enquiring and sceptical minds, particulary in so far as medical science is concerned.

Teaching

• CS3016: Introduction to Functional Programming
• New in 2018/19: CS2016/3D4 Concurrency and Operating Systems

• CS4098 Group Design Project (with John Noll, Meriel Huggard)
• CS4003: Formal Methods (II)
• CS3001: Formal Methods
• CS4011: Functional Programming (with Glenn Strong)
• MM101: Introduction to Programming
• NDS105-II: Concurrency Theory
• 4ICT8: System Modelling and Specification
• 3BA4-II: VLSI Design
• 1ICT4 Computer Technology
• 2BA4-I Microprocessor Design
• 2BA5 Digital Electronics
• 3BA1-II: Numerical Methods

Administration

• School Disability Liaison Officer
• Course Director: Creative and Cultural Entrepreneurship

• Director of Undergraduate Teaching and Learning, School of Computer Science and Statistics
• co-Director (TCD), Lero Graduate Programme (School) in Software Engineering
• Final Year Undergraduate Project Coordinator
• Academic Representative, Library Management System Steering Committee.
• Chair, Trinity Week Academic Symposium.
• Statutory member of the Board of Trinity College Dublin, September 2005-September 2008.
  • Board member of the Information Policy Committee.
  • Chair, Code of Governance Working Group.
• Course Director, BA (Mod.) Information \& Communications Technology, September 2000-September 2006.

Other Activites