Principles of Programming Research Group
The Principles of Programming research group at Maynooth University
specialises in the static analysis and verification of object-oriented
programs and programming languages. The principal investigators in the
We exploit a variety of
techniques, such as parsing, meta-modelling, model-checking and
deductive program verification to increase the reliability of software
systems. Our work has applications in software reliability, program
comprehension and model-driven engineering.
The group's interests extend from software engineering tools
and techniques, right through programming language design, down to the
implementation of compilers and
programming language processors. We have a strong interest
in the formal underpinnings of programming languages, and much of our
work has links with formal methods in program design and
analysis, such as software specification, refinement, verification and
programming language semantics.
For program specification and refinement we use the
Event B modelling language and
also the Why3 environment. These
sit atop a number of theorem-proving tools, but we make most use of
the Z3 SMT solver and
the Coq proof assistant.
We have also used Maude for
for algebraic specification and modelling.
For language and model transformations we use
the Rascal Metaprogramming Language,
or ATL for rule-based model
transformation, and thus
EMF for metamodelling and code generation.
Work by Marie Farrell on using the theory of institutions to give a
semantics for the Event-B specification language resulted in
Code and data are available from her
Research by Andrew Healy on selecting SMT solvers for the Why3 system
is summarised in his
EPTCS paper, and
available from his
Work by Zheng Cheng on verifying ATL transformations is described in
journal paper, and his current work is available from his
The formal MU list for
Alumni: POP graduates
- Marie Farrell, Event-B in the Institutional Framework: Defining a
Semantics, Modularisation Constructs and Interoperability for a
Specification Language, PhD. Thesis, Dept. of
Computer Science, Maynooth University, October 2017.
- Andrew Healy, Predicting SMT solver performance for software verification,
MSc. Thesis, Dept. of Computer Science, Maynooth
University, October 2016.
- Keith Ó Dúlaigh, A Model Driven Approach for Refactoring Heterogeneous
Software Artefacts, MSc. Thesis, Dept. of
Computer Science, Maynooth University, February 2016.
- Zheng Cheng, Formal Verification of Relational Model Transformations using
an Intermediate Verification Language, PhD. Thesis,
Dept. of Computer Science, Maynooth University, September 2015.
- Jagadeeswaran Thangaraj, Adding Ownership Constraints to OCL to automatically generate
Spec# skeletons, MSc. Thesis, Dept. of
Computer Science, Maynooth University, August 2015.
- Hao Wu, Automated Metamodel Instance Generation Satisfying
Quantitative Constraints, PhD. Thesis, Dept. of Computer
Science, NUI Maynooth, October, 2013.
- Jacqueline A. McQuillan,
Using Model Driven Engineering to Reliably Automate the
Measurement of Object-Oriented Software,
PhD. Thesis, Dept. of Computer Science, NUI Maynooth, March,
- Mark Hennessy, A test-driven development strategy for the construction of
grammar-based software, PhD. Thesis, Dept. of
Computer Science, NUI Maynooth, October, 2006.
- Áine Mitchell, An Empirical Study of Run-Time Coupling and Cohesion Software
Metrics, PhD. Thesis, Dept. of Computer Science,
NUI Maynooth, October, 2005.
- Gareth Carter,
Support tools for Object Oriented Software,
MSc. Thesis, Dept. of Computer Science, NUI Maynooth, July 2005.