• PhD., November 2010 (research, by dissertation only)
  Title: Data Refinement in Object-Oriented Verification,
  Supervisor: Prof. J. Morris,
  School of Computer Applications, Dublin City University, Ireland.


• MSc., February 1998 (research, by dissertation only)
  Title: Deduction Based Transformational Programming,
  Supervisor: Dr F. Geiselbrechtinger,
  Department of Computer Science, University College Dublin, Ireland.


• BSc. (Single Hons.), 1995 (Computer Science), 1st Class Honours
  University College Dublin, Belfield, Dublin 4, Ireland.

Research Area: Safety Critical Software, Dependable Software Systems, Specification Languages, Systems Modelling, Formal Methods and Software Verification, and Program Verification Tools, Refinement, Software Analysis, Computer Science Education.

National Priority Areas: CT (Future Networks, Communications and Internet of Things, Robotics and Artificial Intelligence (including Machine Learning) with applications in NPAS concerning software reliability (e.g.s, Medical Devices, Diagnostics, Sustainable Living).

MU Research Theme: Mathematics, Communications and Computation.

MU Research Cluster: Dependable Software and Computation.

Computer Science Research Groups: Principles of Programming, PACT (Programming ⋀ Algorithms ⇒ Computational Thinking).

Projects that I currently lead include:

• MAIVV: Modular AI Verification and Visualisation (SFI Frontiers Frontiers for the Future PROJECT, €620826, 2021-2025), MAIVV provides scalable techniques for software development that guarantee software dependability, when deep learning techniques are employed by developers.

• VALU3S (H2020 ESCEL/Enterprise Ireland, MU component €447,202, 2020-2023), which 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 in Event-B (IRC, €96,000, 2019-2023), which 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.

• CoCoA: Co-create, Collaborate Activate – Advancing Computational Thinking Education (SFI Discover, €149,376, 2021-2022) which provides for teacher training workshops in Computational Thinking, resources for students/teachers, school visits, the Bebras National Competition, and development of our community of practice. The focus is on improving teamwork and collaboration in the classroom through active learning and computational thinking.

• InSPECT: Introducing the Science of Problem-solving through Education in Computational Thinking (SFI Discover, €272,895, 2018-2021), which provides funding to research and develop computational thinking teaching resources and activities, resulting in increased student, teacher, and parent interest and a corresponding enhanced involvement in STEM.

Projects in which I am currently a research partner are:

• A Multi-dimensional Model of Interpreted Language Power Consumption (2020-2022), which 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, co-supervised with Dr Kevin Casey, MU

• TechMate: A best practice toolkit for driving sustainable acceleration towards gender equality in technology disciplines in HEIs (HEA Gender Equality Enhancement Fund 2020, €33,000, 2021), led by Prof. Sarah Jane Delany and Dr. Susan McKeever, School of Computer Science, TU Dublin, supported by MU, IT Carlow and UCD

• Irish Network for Gender Equality in Computing (INGENIC) : The Collective Voice for Gender Equality in Computing HEA Gender Equality Enhancement Fund 2020, € 23,800, 2021), led by Anne Wright, Dept of Technology and Psychology, IADT and supported by MU and GMIT and members of the INGENIC network.

• SFI Centre for Research Training in Foundations of Data Science (SFI, Named PhD Supervisor, 2019-2026)

• SFI Centre for Research Training in Advanced Networks for Sustainable Societies (SFI, Named PhD Supervisor, 2019-2026)

Researcher Mentorship: Funded by SFI, ESCEL JU and EI PhD Supervision: Funded by SFI, IRC and Maynooth University postgraduate Scholarships External PhD examination Research MSc Supervision: Funded by SFI Research Frontiers Grant (2012-2016) and Enterprise Ireland

• Erasmus Mundus Scholars 2013: Dr Kaan Kurtel, Dr Thomas Wies, Dr Petrucio Viana, Dr Sebnem Er.

• Research Brazil Ireland: Dr Petrucio Viana, Dr Marcia Cerioli

• Research Visit: Dr Ruzica Piskac

• Dominique Mery, UHP, Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2009: Lectures presented to the MSc in Computer Science students on Event B and the Rodin platform and a Departmental Seminar on Case studies in Event B.

• Dominique Mery, LORIA, Laboratoire Lorrain de Recherche en Informatique et ses Applications, Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.

• Dominique Cansell, LORIA, Laboratoire Lorrain de Recherche en Informatique et ses Applications, Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.

• Dominique Mery, UHP, Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2008: Lectures presented to the MSc in Computer Science students on Event B and the Rodin platform and a Departmental Seminar on Case studies in Event B.

• Paul Gibson, Le département LOgiciels-Réseaux, Telecom & Management SudParis, Research Visit in 2008 for collaboration on teaching formal methods and presentation of research relating to the ETAPS 2008 publication "How Do I know If My Design Is Correct?"

• K. Rustan M. Leino Microsoft Research, Redmond, Research Collaboration and Research Presentation in 2007: Program verification via an intermediate verification language

• Anna Danko, Polish Japanese Institute of Information Technology, Warsaw, Poland, Research collaboration and presentation of research on Multi Agent Systems (May 11th and 12th, 2004)

• Rem Collier, Department of Computer Science, University College Dublin, Research presentation on Agent Factory: A Framework for the Engineering of Agent-Oriented Applications (9th February 2004)

• John McCormack, Hewlett Packard, Systems Research Labs, Palo Alto, Research collaboration and presentation in 2003.

I am a full time academic in the Department of Computer Science, NUI Maynooth since October 1999. I have been lecturing in Computer Science since 1997 in University College Dublin, Griffith College Dublin and NUI Maynooth. I have also being a visiting lecturer at Universite de Lorraine in France and Zhejiang University in China. Subjects which I have lectured include Software Verification, Rigorous Software development, Type Theory, Models of Computation, Object Oriented Programming (C++, Java, C#), Object Oriented Design, Algorithms and Data Structures, Information Systems Development, Database Management Systems, Computer Graphics, Formal Methods, Program Language Semantics and Discrete Structures. This academic year (2014/2015), I am teaching:

• CS603 - Rigorous Software Development (MSc Level)
• CS629 - Directed Reading (MSc Level)
• CS357 - Software Verification (3rd Year BSc Level)

I also direct the following taught postgraduate programmes:

• Erasmus Mundus Double MSc in Dependable Software Systems - Programme Director from September 2011 to-date on this international level 9 programme funded from 2012 - 2018 by student and teaching scholarships from the European Commission
• MSc in Computer Science (Software Engineering) Director from July 2005-September 2007 and January 2011 to-date on this level 9 programme for full time and part time students
• Postgraduate Diploma in Science (Software Engineering) Director from July 2005-September 2007 and January 2011-September 2013 on this level 9 programme for full time and part time students
• International Student Exchange Coordinator August 2004 – December 2005

Some (old) lecture slides follow. New lecture slides are available on Moodle.

CS101 Introduction to Programming - see https://firstyears.cs.may.ie/

CS603 Rigorous Software Process – see MSc Lab J drive

CS613 Object-Oriented Programming and C++

Se202 Algorithms and Data Structures

SE119 Discrete Structures

SE304/CS407 Formal Methods (Z Specification & Program Verification)

SE424 Formal Methods (Program Language Semantics)

• Deductive Verification Systems, Evaluating Software Verification Systems: Benchmarks and Competitions, Dagstuhl seminar 14171, 2014

• Evaluating Software Verification Systems, Foundations of Computer Science Seminar Series, Dept. of Computer Science, NUIM,2014

• An early program proof by Turing, Turing Year Seminars, Dept. of Computer Science, NUIM, 2012

• Case Based Specifications: reusing specifications, programs and proof, AI meets Formal Software Development, Dagstuhl seminar 12271, 2012

• Teaching Using Spec# in Europe: A Experience Report from University Teaching and Various Verification Tutorials, Microosft Faculty Summit, 2011

• Encoding Comprehensions as First Order Expressions in Boogie, Programming Languages and Methods Group Meeting, Microsoft Research, Redmond, WA, USA, February 2008

• Automatic Verification of C# programs, Staff Seminar Series Department of Computer Science, NUI Maynooth, Ireland , November 2007

• Automatic Program Verification with Spec#, MOSEL Research Seminar Series, LORIA, Nancy, France, May 2007

• Automatic verification of textbook programs that use comprehensions, Formal Techniques for Java-like Programs, Berlin, Germany , July 2007

• Software Refinement with Perfect Developer, Software and Systems Engineering Seminar Series, NUI Maynooth, (December 2005)

• Problem-Based Learning: A Hybrid Model, Department of Computer Science, Clemson University, (June 2005)

• Typing in Object Oriented Languages, NUIM/DCU Seminar series, NUI Maynooth, (April 2001)

• A DEBATE with Isabelle, Dept. of Computer Science, NUI Maynooth, (November 1999)

• Tactics for Transformational Programming, IWFM '97, University College Dublin, (July 1997)

• Proving Transformations in Isabelle, IFMSIG Meeting, University College Cork, (November 1996)

• Program Construction by Transformations", Postgraduate Day, University College Dublin, (November 1996)

• Transformational Programming, Dept. of Computer Science, University College Dublin, (September 1996)

• Transformational Programming, Dept. of Computer Science, Technical University Munich, (July 1996)

• Microsoft Research, Redmond, WA, USA, Gratis Visitor to Microsoft Research in 2008 to prepare a tutorial on the Spec# Programming System for presentation at ETAPS 2008, to develop material for the MSc curriculum in Computer Science and to further ongoing research collaboration.

• Trampower UK, We apply reverse-engineering techniques to an already existing tram control system, with the overall aim of verifying the correctness of its safety critical properties. We are developing tools to translate the control system from Programmable Logic to Event B.

• Microsoft Research, Redmond, WA, USA, This research extended the Spec# programming system, increasing the categories of programs that this system could verify using the SMT solvers Simplify and Z3. In particular, we focused on extending the system so that it could be used with typical examples used in program verification

• Escher Technologies, UK Review of the support for Refinement within the Perfect language and Perfect Developer Toolset (2003-2006)

• Hewlett Packard, Systems Research Labs, Palo Alto, Collaboration on Programming Language Design (2003)

• Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2009: Lectures on the Spec# Programming System

• Institute of Cybernetics, Tallinn University of Technology, To attend COST Action IC0701, Winter School on Verification of Object-Oriented Programs ran by a European network of researchers working on methods and tools for verification.

• Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), France , Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.

• Dublin City University, Collaboration with Prof J. Morris on Data Refinement in Object Oriented Languages.

• MOSEL Research Group, Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Research on the formal verification and refinement of software systems using the Event-B methodology.