Dr Rosemary Monahan

image

Contact Details

Rosemary Monahan, Associate Professor,
Room 127, Eolas Building, North Campus
Address: Department of Computer Science, NUI Maynooth, Maynooth Co. Kildare
image
Phone Number: +353-1-7083463/3847

Qualifications

  • 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 Interests

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).

Research Funding

Funded projects that I currently lead include:

  • 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.
Funded projects in which I am currently a research partner are:

  • 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)

Research Supervision

PhD Supervision: Funded by 4 IRC postgraduate awards and 2 MU PhD Scholarships
  • 2019 - 2023 C Reynolds, A Constructive Framework for Software Specification and Refinement (Supervisor, IRC scholarship doctoral €96,000)
  • 2020 - 2021 J Lambert, A Multi-dimensional Model of Interpreted Language Power Consumption (Co-Supervisor)
  • 2013 - 2017 M Farrell, Integrating Software Models (Lead Supervisor, IRC scholarship doctoral €96,000)
  • 2011 - 2015 Z Cheng, Formal Verification of Relational Model Transformations using an Intermediate Verification Language (Lead Supervisor, Teaching doctoral scholarship €84,000)
  • 2009 - 2013 H Wu, Automated Metamodel Instance Generation (Co-Supervisor, John Hume Scholarship)
External PhD examination
  • Towards a practically extensible Event-B methodology, Issam Maamria, University of Southampton, UK, 2012
Research MSc Supervision: Funded by SFI Research Frontiers Grant (2012-2016) and Enterprise Ireland
  • 2016 A Healy, Predicting SMT solver performance for software verification (Co-supervisor, SFI RFP funded)
  • 2016 K Dooley, A MDE approach for Refactoring Software Systems (Co-supervisor, SFI RFP funded)
  • 2015 J Thangaraj, Adding Ownership Constraints to OCL (Lead Supervisor, SFI RFP funded)
  • 2006 Gareth Carter, Support tools for Object Oriented Software Development (Supervisor, Enterprise Ireland Basic Research funded)

Research Visitors Hosted

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

Professional Assignments

DESEM Erasmus Mundus Consortium Director 2012-2018

Academic Member of the Senate of the National University of Ireland 2007-2017 (Elected for 2 consecutive terms by the NUIM Governing Authority, NUI Maynooth)


Membership of NUI Maynooth Committees

  • ENACTUS NUI Maynooth (Invited Academic Advisor, 2012-to date)
  • Capitation Committee (Nominated, 2002-to date)
  • Governing Authority (Elected, 2000-2005)
  • Human Resources Committee (Nominated, 2000-2005)
  • Student Affairs Committee (Nominated, 2000-2005)


Member of the Program Committee/ Reviewer for

  • 21st Workshop on Foundations of Object-Oriented Languages (FOOL) 2014
  • The International Journal on Software Tools for Technology Transfer (STTT) 2014
  • 19th International Symposium on Formal Methods (FM) 2014
  • 11th International Colloquium on Theoretical Aspects of Computing (ICTAC) 2014
  • 19th International Conference on Engineering of Complex Computer Systems (ICECCS) 2014
  • Formal Techniques for Java-like Programs (FTfJP) 2009, 2011 and 2013
  • 28th ACM Symposium on Applied Computing, Special track on Object Oriented Programming Languages and Systems(SAC OOPS) 2013
  • 1st International Workshop on Automated Reasoning in Software Verification (ARiSVe) 2013 (postponed)
  • 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE) 2013
  • International Conference on Formal Verification of Object-Oriented Software (FoVeOOS) 2010 and 2011
  • International Conference on Engaging Pedagogy (ICEP) 2011
  • China-Ireland International Conference on Information and Communication Technologies (CIICT) 2009
  • Verification, Model Checking, and Abstract Interpretation (VMCAI) 2009
  • Principles and Practice of Programming in Java (PPPJ) 2002, 2003 and 2008
  • ACM Symposium on Applied Computing (SAC) 2002, 2012 and 2013


Principal Organiser for:

  • DESEM MSc Summerschool, 2013
  • 7th Management Committee & Working Group Meeting, Cost Action IC0701, 2011
  • Cost Action IC0701 PhD Training School, 2011


Member of the Organising Committee for

  • Principles and Practice of Programming in Java (PPPJ) 2003
  • Irish Workshop in Formal Methods, 1997 and 2002


External Examiner for

  • Towards a Practically Extensible Event-B Methodology, Issam Maamria, PhD thesis, Univsirt of Southampton, 2012
  • BA Mathematics modules, Dublin Business School (2006-2009)
  • MSc in Computing Science, Griffith College Dublin (2005-2008)


Other Activities

  • Irish representative in trhe European Scientfic COST Action IC0701
  • NUI Travelling Studentships in Science Awarding Panel
  • Committee Member and Adjudicator, ICS Robocode Ireland Challenge, Tipperary Institute (2006- to 2010)
  • Grand Challenge Maths Initiative demonstration lecture and school liaison, Coláiste Bride, Dublin (2005)
  • Independent Reviewer of the TYPES project (Coordination Action FP6 2002 IST-C)
  • PhD Viva Chair (Dr S Bergin 2006, Dr P Corcoran 2008)

Teaching and Academic Programme Directorships

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:

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)

Research Presentations

  • 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)

Industrial Collaboration

  • 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)

Academic Collaboration

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

Publications

See here for details.

loading