Rosemary Monahan is interested in the study of existing object-oriented specifications, object oriented programming languages and object encodings, with particular emphasis on type theory.
James Power works with compiler technology for object-oriented languages, with an emphasis on program comprehension and dynamic analysis.
Marie Farrell's research seeks to integrate the process of formal refinement into the model-driven engineering approach, so that models expressed in different modelling languages, formalisms and tools can be combined within one formal framework in a provably correct way. At the moment she is working on the construction of an institution-based specification of the Event-B formalism.
Andrew Healy is working in the area of formal verification, particularly approaches using SMT solvers (via the Why3 platform). His particular concern is with the modularisability of program verification, and how this related to modularity between and within theories in SMT solvers.
Formalised EMFTVM bytecode language for sound verification of model transformations
Modularising and Promoting Interoperability for Event-B Specifications using Institution Theory
Evaluating the Use of a General-Purpose Benchmark Suite for Domain-Specific SMT-solving
A sound execution semantics for ATL via translation validation
Creating Formal Specifications with Analogical Reasoning
An early completion algorithm: Thue's 1914 paper on the transformation of symbol sequences