The Principles of Programming research group at Maynooth University specialises in the static analysis and verification of programs and programming languages.
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.
Recent highlights
- Research from the VALU3S Aerospace use-case formalising requirements for an aircraft engine controller accepted for publication at REFSQ 2022 .
- A methodology for developing a verifiable Aircraft Engine Controller from formal requirements accepted for publication at IEEE Aerospace Conference .
- Work by Marie Farrell on using the theory of institutions to give a semantics for the Event-B specification language resulted in publications at WADT , ICFEM and SEFM . Code and data are available from her GitHub repo .
- Research by Andrew Healy on selecting SMT solvers for the Why3 system is summarised in his EPTCS paper, and available from his GitHub repo .
- Work by Zheng Cheng on verifying ATL transformations is described in his SoSym journal paper , and his current work is available from his GitHub repo .
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 algebraic specification and Hets 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.
We welcome interest from Postdoctoral Researchers and prospective PhD students who wish to collaborate with us on research funding proposals. Funded applications will be advertised via Maynooth University Vacancies
Current Group Members
The principal researchers in the group are:- Rosemary Monahan , Professor
- Barak A. Pearlmutter , Professor
- Hao Wu , Assistant Professor
- Kevin Casey , Assistant Professor
- Medet Inkarbekov, PostDoctorate Researcher
- Syed Ali Asadullah Bukhari, PostDoctorate Researcher
- Conor Reynolds , PhD Student (supervised by Rosemary)
- Jonathan Lambert , PhD Student (co-supervised by Rosemary and Kevin)
- Oisin Sheridan , PhD Student (supervised by Rosemary)
- Dara MacConville , PhD Student (supervised by Rosemary)
- Thomas Flinkow, PhD Student (supervised by Rosemary and Barak)
- Ankit Jha, PhD Student (supervised by Hao and Rosemary)
- Huan Zhang, PhD Student (supervised by Hao)
Previous Members:
- Marie Farrell , Senior PostDoctorate Researcher on VALU3S project 2020-2022
- Matthew Luckcuck , PostDoctorate Researcher on VALU3S project 2020-2022
- James Power (deceased, 2019), one of the founders and a principal researcher in the Principles of Programming research group was an expert in specification and program analysis, with a particular emphasis on the foundations of software engineering, including metamodelling and language design. His contributions continue to inspire our research.
The Maynooth University publication list for Rosemary Monahan is available at: https://www.maynoothuniversity.ie/computer-science/our-people/rosemary-monahan#3 . The Maynooth University publication list for James Power is available at: https://www.maynoothuniversity.ie/computer-science/our-people/james-power#3 .
Current Projects
- MAIVV:Modular AI Verification and Visualisation (2021-2025), researching scalable techniques for software development that guarantee software dependability, even when deep learning techniques are employed by developers. We focus on a methodology to verify properties of hybrid systems with mixed discrete and continuous dynamics, and associated software tooling to integrate this with existing verification frameworks. Led by Dr Rosemary Monahan in collaboration with Professor Barak A. Pearlmutter .
- VALU3S (2020-2023) , designs and implements process workflows and tools for improving the time and cost needed in verification and validation of automated systems. Funded by Enterprise Ireland and H2020 ESCEL, MU is collaborating with United Technology Research Center (UTRC) to improve workflows and tools for verification and validation of an aircraft engine controller.
- A Constructive Framework for Software Specification and Refinement (2019-2023), builds on our mathematical foundation for model-driven software engineering, and provides a well-developed formal infrastructure to ensure the usability and the integrity of the approach.
- A Multi-dimensional Model of Interpreted Language Power Consumption (2020-2022), examines interpreted language performance and focus on the integration and synthesis of models from a high level code perspective, through to their intermediate representations, the virtual machines that provide platform independence, and across the juncture between these virtual machines and the processor core.
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, 2011.
- 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.
