Dr Rosemary Monahan

    Computer Science, Hamilton Institute

    Gaeilge agus fáilte

    Associate Professor

    Eolas Building
    1st Floor
    127
    (01) 708 3463
    http://rosemarymonahan.com/

    Biography

    Dr Rosemary Monahan an associate professor in the Department of Computer Science and an affiliate of the Hamilton Institute at Maynooth University. She holds BSc and MSc degrees in Computer Science from UCD and a PhD from DCU.

    Dr Monahan is a founding member of the Principles of Programming research group which specialises in the static and dynamic analysis of software. She has expertise in the modelling, analysis and verification of software and programming languages, working with international academics and industry to develop and employ techniques increasing the dependability of software systems (such as those in the medical, automotive, and aerospace domains). 

    Dr Monahan is co-founder of the international VerifyThis competition series, bringing together both academic and industrial users of tools which guarantee the correctness and reliability of software systems. She is currently funded by Science Foundation Ireland Frontiers for the Future to verify AI based-systems (MAIVV, 2021-2025) and Enterprise Ireland and H2020 ESCEL JU programme to improve workflows and tools for verification and validation of an aircraft engine controller (Valu3s, 2020-2023). She is passionate about providing solid mathematical foundations for software systems and in next-generation verification technologies applied to AI-based software. “Arís: Analogical Reasoning for reuse of Implementation & Specification” is a recent project concerning applying models of analogical reasoning to the domain of reliable software development and re-use.

    Dr Monahan is PI on two SFI Discover projects on the PACT group, producing educational resources that teach the science of problem-solving through computational thinking (InSPECT, 2019-2022) and (CoCoA, 2021-2022). She is a named supervisor in the SFI Centre for Research Training in Foundations of Data Science and the SFI Centre for Research Training in Advanced Networks for Sustainable Societies, and supervises PhD students funded by the Irish Research Council. 

    As the Director of the Erasmus Mundus MSc in Dependable Software Systems (2012-2018), she has secured and managed €2.5 million in EU funding, providing foundations for the subsequent DEPEND Erasmus Mundus programme. Recent collaborators include UTRC, Ireland; Microsoft Research, USA; Amazon Web Services, USA; and INRIA, France; with research funded via the Irish Research Council, Science Foundation Ireland, Enterprise Ireland, and Horizon 2020.

    Research Interests

    Research Interests: 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.
    .

    Research Projects

      Project Role Funding Body / Program Description Start Date End Date Award (€)
    MAIVV: Modular AI Verification and Visualisation PI Science Foundation Ireland / Frontiers for the Future PROJECT MAIVV provides scalable techniques for software development that guarantee software dependability, when deep learning techniques are employed by developers. As society increases reliance on AI-based automated devices, such as driverless cars and IoT connected devices, the need for scalable techniques guaranteeing software dependability becomes urgent, both in terms of human life and the economic cost of software failure. This project combines approaches from software engineering and artificial intelligence to produce software development techniques that provide such guarantees. This research will provide a solid foundation for trustworthy and transparent A.I. by (1) building a solid theoretical bridge between logic-based verification and deep learning systems, (2) providing a practical demonstration of the benefits of this integration and (3) exploiting techniques from program comprehension to understand deep learning code. 01-DEC-21 30-NOV-25 620826.6
    TechMate A best practice toolkit for driving sustainable acceleration towards gender equality in technology disciplines in HEIs Collaborator Higher Education Authority / 01-JAN-21 31-DEC-21 33000
    INGENIC: Irish Network for Gender Equality in Computing Collaborator Higher Education Authority / 01-JAN-21 31-DEC-21 23800
    CoCoA: Co-create Collaborate Activate - Advancing Computational Thinking Education PI Science Foundation Ireland / Discover Programme CoCoA promotes engagement in Computational Thinking (CT) as a vehicle to improve scientific problem solving skills through three core activities: - Co-creation: we co-create teaching materials through collaboration with in-service and pre-service teachers to produce lesson plans providing both traditional CT tasks and active learning tasks for a classroom setting; guidance notes to teachers; and CT resource books - Collaboration: Our resources facilitate teamwork among peers giving students the mechanisms and language necessary for collaborative problem solving and reflection. - Activation: we co-develop active CT games as a way to facilitate active learning 01-JAN-21 31-DEC-22 149375.77
    VALU3S - Verification and Validation of Automated Systems' Safety and Security (Stage 2) PI EU Horizon 2020 / ECSEL Joint Work Plan (co-funded with Enterprise Ireland) VALU3S evaluates the state-of-the-art in Verification and Validation (V&V) methods and tools, and designs a multi-domain framework to create a clear structure around the components and elements needed to conduct the V&V process. The expected benefit is to reduce time and cost needed to verify and validate automated systems with respect to safety, cyber-security, and privacy requirements. In VALU3S, 13 use cases with specific safety, security and privacy requirements are studied in detail. MU is collaborating with United Technology Research Center (UTRC) on the Aerospace use-case, improving workflows and tools for verification and validation of an aircraft engine controller. 01-MAY-20 30-APR-23
    InSPECT: Introducing the Science of Problem-solving through Education in Computational Thinking PI Science Foundation Ireland / Discover Programme InSPECT researches and develops computational thinking teaching resources and activities, resulting in increased student, teacher, and parent interest and a corresponding enhanced involvement in STEM. Our team combines their prior experience in liaising with schools with their expertise in Computational Thinking pedagogy to engage our target audience with Computational Thinking. We achieve this through teaching resources (lesson plans, workbooks, teacher portal) building upon carefully curated Bebras problems, and activities (workshops, school visits, and regional meetups). The result is increased teacher, student, and parent interest and a corresponding enhanced involvement in STEM subjects. 01-JAN-19 31-DEC-21 272895
    A constructive framework for software specification and refinement in Event-B / Conor Reynolds PI Irish Research Council (IRC) / Government of Ireland Postgraduate Scholarship Two central issues in modern software development are controlling the complexity of large software systems and ensuring their reliability. Model-driven engineering (MDE) mitigates complexity by allowing different aspects of a system to be modelled from different perspectives and at different levels of granularity. Software verification offers the prospect of developing code that meets formal specifications, thus enhancing its reliability. The theory of institutions offers the unification of MDE with verification, and ensures consistency between different software models. The cost is that it can be difficult to set up a formalism in the theory of institutions, and to ensure that your encoding satisfies the constraints of that theory. This research addresses this problem by harnessing cutting-edge international research in higher-order logic to develop the theory and practical tools to construct institutions. It builds on existing local expertise with industrial-strength formal methods that have been used for air-traffic control systems, train interlocking systems and medical devices. This in turn will enable software engineers to integrate models from different formalisms and thus help to verify that software meets its specifications. 01-SEP-19 31-AUG-23 105333.12
    Building Reliable Software Systems – Software Refinement meets Software Verification PI Irish Research Council for Science, Engineering and Technology / IRCSET / Ulysses travel scheme 01-JAN-13 31-DEC-13
    Request for travel fund for a workshop, May 6 – 9 2014, Lorenz Center, Leiden, The Netherlands PI EU Horizon 2020 National Support Network / Travel Assistance 06-MAY-14 09-MAY-14
    A Logical Framework for Integrating Software Models via Refinement. PI Irish Research Council (IRC) / Government of Ireland Postgraduate Scholarship In this research we ask how we can correctly combine information from models which focus on different aspects of the software system, so that the software system as a whole can be modeled through their integration. The central aim is to establish a theoretical framework within which refinement steps, and their associated proof obligations, can be shared between different formalisms. Our core hypothesis is that the theory of institutions can provide this framework and, to this end, we propose to construct an institution-based specification of the Event-B formalism. 01-OCT-13 30-SEP-17 95680
    FMICS/iFM 2018 PI Science Foundation Ireland / Conference & Workshop Grants FMICS is a 2 day conference on applying Formal Methods to Industrial Critical Systems. iFM is a 3 day conference on intergrated Formal Methods. Both conferences will be hosted in MU from Sept 3 - 7 2018. 08-AUG-18 07-SEP-18 10370
    FMICS/iFM 2018 Conferences PI Failte Ireland / Conference Ambassador FMICS/iFM are conference that I will host at MU from Sept 3rd - 7th. 03-SEP-18 07-SEP-18 1400

    Post Doctoral Fellows/Research Team

      Researcher Name Project Role Funding Body
    Marie Farrell VALU3S: Verification and Validation of Automated Systems’ Safety and Security Post Doctorate EU Horizon 2020
    Dara John Dillon Andrea Mac Conville Verification of Robotic Systems Postgraduate student Science Foundation Ireland
    Taina Marja Lehtimaki CoCoA:Co-create, Collaborate Activate – Advancing Computational Thinking Education Research Assistant Science Foundation Ireland
    Taina Marja Lehtimaki InSPECT: Introducing the Science of Problem-solving through Education in Computational Thinking Research Assistant Science Foundation Ireland
    Jonathan Mark Lambert A Multi-dimensional Model of Interpreted Language Power Consumption Postgraduate student
    Oisin Sheridan VALU3S: Verification and Validation of Automated Systems’ Safety and Security Postgraduate student EU Horizon 2020
    Conor Reynolds A constructive framework for software specification and refinement in Event-B Postgraduate student Irish Research Council (IRC)
    Matthew Luckcuck VALU3S: Verification and Validation of Automated Systems’ Safety and Security Post Doctorate EU Horizon 2020

    Book Chapters

      Year Publication
    2015 'A Sound Execution Semantics for ATL via Translation Validation'
    Dr Rosemary Monahan (2015) 'A Sound Execution Semantics for ATL via Translation Validation' In: Theory and Practice of Model Transformations . L'Aquila, Italy: Springer. [full-text] [Details]
    2010 'Dafny Meets the Verification Benchmarks Challenge'
    Dr Rosemary Monahan, Dr K Rustan M Leino (2010) 'Dafny Meets the Verification Benchmarks Challenge' In: Verified Software: Theories, Tools, Experiments. Edinburgh, UK: Springer. [full-text] [Details]

    Peer Reviewed Journals

      Year Publication
    2021 'VerifyThis 2019: a program verification competition'
    Dross C.;Furia C.A.;Huisman M.;Monahan R.;Müller P. (2021) 'VerifyThis 2019: a program verification competition'. International Journal on Software Tools for Technology Transfer, [DOI] [Details]
    2021 'Power Consumption Profiling of a Lightweight Development Board: Sensing with the INA219 and Teensy 4.0 Microcontroller'
    Lambert, Jonathan and Monahan, Rosemary and Casey, Kevin (2021) 'Power Consumption Profiling of a Lightweight Development Board: Sensing with the INA219 and Teensy 4.0 Microcontroller'. Electronics, 10 (7) [DOI] [full-text] [Details]
    2017 'Predicting SMT Solver Performance for Software Verification'
    Healy, A;Monahan, R;Power, JF (2017) 'Predicting SMT Solver Performance for Software Verification'. Electronic Proceedings In Theoretical Computer Science, :20-37 [DOI] [full-text] [Details]
    2017 'VerifyThis 2015: A program verification competition'
    Huisman M.;Klebanov V.;Monahan R.;Tautschnig M. (2017) 'VerifyThis 2015: A program verification competition'. International Journal on Software Tools for Technology Transfer, 19 (6):763-771 [DOI] [full-text] [Details]
    2016 'Formalised EMFTVM bytecode language for sound verification of model transformations'
    Cheng Z.;Monahan R.;Power J. (2016) 'Formalised EMFTVM bytecode language for sound verification of model transformations'. Software and Systems Modeling, :1-29 [DOI] [full-text] [Details]
    2015 'VerifyThis 2012: A Program Verification Competition'
    Huisman M.;Klebanov V.;Monahan R. (2015) 'VerifyThis 2012: A Program Verification Competition'. International Journal on Software Tools for Technology Transfer, 17 (6):647-657 [DOI] [full-text] [Details]

    Other Journals

      Year Publication
    2022 'Towards Refactoring FRETish Requirements'
    Marie Farrell and Matt Luckcuck and Oisin Sheridan and Rosemary Monahan (2022) 'Towards Refactoring FRETish Requirements' arXiv:2201.04531 [cs.SE], . [Details]
    2022 'FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller'
    Marie Farrell and Matt Luckcuck and Oisin Sheridan and Rosemary Monahan (2022) 'FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller' arXiv:2112.04251 [cs.SE], . [Details]
    2021 'Building Specifications in the Event-B Institution'
    Marie Farrell and Rosemary Monahan and James F. Power (2021) 'Building Specifications in the Event-B Institution' arXiv preprint arXiv:2103.10881 [cs.LO], . [Details]
    2021 'VerifyThis 2019: A Program Verification Competition (Extended Report)'
    Claire Dross and Carlo A. Furia and Marieke Huisman and Rosemary Monahan and Peter Müller (2021) 'VerifyThis 2019: A Program Verification Competition (Extended Report)' arXiv:2008.13610 [cs.LO], . [Details]
    2021 'A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements'
    Matt Luckcuck and Marie Farrell and Oisín Sheridan and Rosemary Monahan (2021) 'A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements' arXiv:2110.09277 [cs.SE], . [Details]
    2019 'Proceedings Fifth Workshop on Formal Integrated Development Environment'
    Monahan R.;Prevosto V.;Proença J. (2019) 'Proceedings Fifth Workshop on Formal Integrated Development Environment' Electronic Proceedings in Theoretical Computer Science, EPTCS, 310 . [DOI] [Details]
    2018 'Proceedings 4th Workshop on Formal Integrated Development Environment'
    Masci P.;Monahan R.;Prevosto V. (2018) 'Proceedings 4th Workshop on Formal Integrated Development Environment' Electronic Proceedings in Theoretical Computer Science, EPTCS, 284 . [DOI] [Details]
    2012 'Metamodel Instance Generation: A systematic literature review'
    Hao Wu and Rosemary Monahan and James F. Power (2012) 'Metamodel Instance Generation: A systematic literature review' arXiv:1211.6322 [cs.SE], . [full-text] [Details]
    2020 'VerifyThis 2019: A Program Verification Competition (Extended Report)'
    Claire Dross and Carlo A. Furia and Marieke Huisman and Rosemary Monahan and Peter Müller (2020) 'VerifyThis 2019: A Program Verification Competition (Extended Report)' arXiv preprint arXiv:2008.13610, . [Details]

    Conference Publications

      Year Publication
    2021 Upcycling formal specifications for similar implementations with Arís
    Aiyankovil K.G.;Monahan R.;O’Donoghue D.P. (2021) Upcycling formal specifications for similar implementations with Arís CEUR Workshop Proceedings , pp.90-91 [Details]
    2021 Using dafny to solve the VerifyThis 2021 challenges
    Farrell M.;Reynolds C.;Monahan R. (2021) Using dafny to solve the VerifyThis 2021 challenges FTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021 , pp.32-38 [DOI] [full-text] [Details]
    2018 An Approach to Combining the Institutions for Event-B and Temporal Logic
    Marie Farrell and Rosemary Monahan and James F. Power and Michael Fisher (2018) An Approach to Combining the Institutions for Event-B and Temporal Logic 24th International Workshop on Algebraic Development Technique Royal Holloway University of London, [full-text] [Details]
    2018 Proceedings 4th Workshop on Formal Integrated Development Environment Oxford, England, 14 July 2018 Preface
    Masci, P;Monahan, R;Prevosto, V (2018) Proceedings 4th Workshop on Formal Integrated Development Environment Oxford, England, 14 July 2018 Preface ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE [Details]
    2017 Specification Clones: An Empirical Study of the Structure of Event-B Specifications
    Marie Farrell and Rosemary Monahan and James F. Power (2017) Specification Clones: An Empirical Study of the Structure of Event-B Specifications International Conference on Software Engineering and Formal Methods Trento, Italy, , 04-SEP-17 - 08-SEP-17 , pp.152-167 [DOI] [full-text] [Details]
    2017 An Institution for Event-B
    Farrell M.;Monahan R.;Power J. (2017) An Institution for Event-B Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , pp.104-119 [DOI] [Details]
    2017 Combining Event-B and CSP: An institution theoretic approach to interoperability
    Marie Farrell, Rosemary Monahan and James F. Power (2017) Combining Event-B and CSP: An institution theoretic approach to interoperability International Conference on Formal Engineering Methods Xi'an, China, , 13-NOV-17 - 17-NOV-17 , pp.140-156 [DOI] [full-text] [Details]
    2017 An Institution for Event-B
    Marie Farrell and Rosemary Monahan and James F. Power (2017) An Institution for Event-B Recent Trends in Algebraic Development Techniques , pp.104-119 [full-text] [Details]
    2016 On Two Friends for Getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in RODIN
    Cheng, Z;Mery, D;Monahan, R (2016) On Two Friends for Getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in RODIN LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I , pp.821-838 [DOI] [full-text] [Details]
    2016 Predicting SMT solver performance for software verification
    Andrew Healy, Rosemary Monahan, and James F. Power. (2016) Predicting SMT solver performance for software verification 3rd Workshop on Formal Integrated Development Environment Limassol, Cyprus, , pp.20-37 [DOI] [full-text] [Details]
    2016 Providing a Semantics and Modularisation Constructs for Event-B using Institutions
    Marie Farrell and Rosemary Monahan and James F. Power (2016) Providing a Semantics and Modularisation Constructs for Event-B using Institutions 23rd International Workshop on Algebraic Development Techniques Gregynog, Wales, [Details]
    2016 Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving
    Andrew Healy and Rosemary Monahan and James F. Power (2016) Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving 31st ACM Symposium on Applied Computing Pisa, Italy, , pp.1558-1561 [DOI] [full-text] [Details]
    2015 Characterising the workload of SMT solvers for program verification
    Andrew Healy and Rosemary Monahan and James Power (2015) Characterising the workload of SMT solvers for program verification 22nd Workshop on Automated Reasoning Birmingham, UK, , pp.17-18 [Details]
    2015 A Sound Execution Semantics for ATL via Translation Validation Research Paper
    Cheng, Z;Monahan, R;Power, JF (2015) A Sound Execution Semantics for ATL via Translation Validation Research Paper 8th INTERNATIONAL CONFERENCE ON THEORY AND PRACTICE OF MODEL TRANSFORMATIONS , pp.133-148 [DOI] [full-text] [Details]
    2015 Verifying SimpleGT Transformations Using an Intermediate Verification Language
    Zheng Cheng and Rosemary Monahan and James F. Power (2015) Verifying SimpleGT Transformations Using an Intermediate Verification Language 4th International Workshop on the Verification Of Model Transformations L'Aquila, Italy, , pp.12-19 [full-text] [Details]
    2014 PACT: An initiative to introduce Computational Thinking in to second level education
    Aidan Mooney and Joseph Duffin and Thomas Naughton and Rosemary Monahan and James Power and Phil Maguire (2014) PACT: An initiative to introduce Computational Thinking in to second level education International Conference on Engaging Pedagogy Athlone, Ireland, [Details]
    2014 Creating Formal Specifications with Analogical Reasoning
    D P ODonoghue, R Monahan, D Grijincu, M Pitu, F. Halim, F Rahman, Y Abgaz, D Hurley (2014) Creating Formal Specifications with Analogical Reasoning C3GI 2014 [full-text] [Details]
    2013 Exploiting attributed type graphs to generate metamodel instances using an SMT solver
    Wu, H;Monahan, R;Power, JF (2013) Exploiting attributed type graphs to generate metamodel instances using an SMT solver 2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE) , pp.175-182 [DOI] [full-text] [Details]
    2013 Transforming Event B Models into Verified C# Implementations
    Dr Rosemary Monahan, Prof Dominique Mery (2013) Transforming Event B Models into Verified C# Implementations Verification and Program Transformation 2013 [full-text] [Details]
    2012 On the Organisation of Program Verification Competitions
    Huisman Marieke, Vladimir Klebanov, Rosemary Monahan (2012) On the Organisation of Program Verification Competitions Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems , pp.50-59 [full-text] [Details]
    2012 The COST IC0701 verification competition 2011
    Bormer T.;Brockschmidt M.;Distefano D.;Ernst G.;Filliâtre J.;Grigore R.;Huisman M.;Klebanov V.;Marché C.;Monahan R.;Mostowski W.;Polikarpova N.;Scheben C.;Schellhorn G.;Tofan B.;Tschannen J.;Ulbrich M. (2012) The COST IC0701 verification competition 2011 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , pp.3-21 [DOI] [full-text] [Details]
    2012 A Simple Complexity Measurement for Software Verification and Software Testing 28-31
    Monahan, Dr Rosemary Zheng Cheng, Dr James F. Power (2012) A Simple Complexity Measurement for Software Verification and Software Testing 28-31 Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012) , pp.28-31 [full-text] [Details]
    2011 nExaminer: A Semi-automated Computer Programming Assignment Assessment Framework for Moodle
    Monahan Rosemary, Zheng Cheng, Aidan Mooney (2011) nExaminer: A Semi-automated Computer Programming Assignment Assessment Framework for Moodle ICEP 2011 [full-text] [Details]
    2011 The 1st Verified Software Competition, Extended Experience Report.
    Klebanov Vladimir, Peter Mller, Natarajan Shankar, Gary T. Leavens, Valentin Wstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss. (2011) The 1st Verified Software Competition, Extended Experience Report. Formal Methods 2011 [full-text] [Details]
    2010 Using ATL in a tool-chain to calculate coverage data for UML class diagrams
    Monahan Rosemary, Power James, Wu Hao (2010) Using ATL in a tool-chain to calculate coverage data for UML class diagrams 2nd International Workshop on Model Transformation with ATL (MtATL 2010) [full-text] [Details]
    2010 Implementing the Verified Software Initiative Benchmarks using Perfect Developer
    Monahan, Rosemary; Xu Yan (2010) Implementing the Verified Software Initiative Benchmarks using Perfect Developer CIICT 2010 [full-text] [Details]
    2010 Dafny meets the verification benchmarks challenge
    Leino K.;Monahan R. (2010) Dafny meets the verification benchmarks challenge Lecture Notes in Computer Science. Proceedings of VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS , pp.112-126 [DOI] [Details]
    2010 Using Boogie 2 in the Verification of Spec# Programs
    Leino, K. Rustan M. and Monahan, Rosemary (2010) Using Boogie 2 in the Verification of Spec# Programs 13th Brazilian Symposium on Formal Methods (SBMF 2010), Brazil 2010 [Details]
    2010 Using ATL in a tool-chain to calculate coverage data for UML class diagrams
    Wu H.;Monahan R.;Power J. (2010) Using ATL in a tool-chain to calculate coverage data for UML class diagrams CEUR Workshop Proceedings , pp.60-64 [full-text] [Details]
    2009 Program Verification Using the Spec# Programming System
    Leino, K. Rustan M. and Monahan, Rosemary (2009) Program Verification Using the Spec# Programming System ECOOP (Summerschool, 9th July 2009, Genoa, Italy) [Details]
    2009 Reasoning about Comprehensions with First-Order SMT Solvers
    Leino, K. Rustan M. and Monahan, Rosemary (2009) Reasoning about Comprehensions with First-Order SMT Solvers 24th Annual ACM Symposium on Applied Computing [full-text] [Details]
    2008 Program Verification Using the Spec# Programming System
    Leino, K. Rustan M. and Monahan, Rosemary (2008) Program Verification Using the Spec# Programming System ETAPS (Spec# Tutorial, Budapest, Hungary, March 2008) [Details]
    2007 Automatic verification of textbook programs that use comprehensions
    Leino, K. Rustan M. and Monahan, Rosemary (2007) Automatic verification of textbook programs that use comprehensions Formal Techniques for Java-Like Programs, ECOOP Workshop, Berlin, Germany, July 2007 [full-text] [Details]
    2006 The Relevance of Scientific Reasoning Skills to Computer Science: A Comparative Study between the US and Ireland
    Parham J.R., O' Kelly J., Monahan R., Stevenson D.E. (2006) The Relevance of Scientific Reasoning Skills to Computer Science: A Comparative Study between the US and Ireland International Conference on Frontiers in Education: Computer Science and Computer Engineering, Las Vegas, USA, 26-29 June 2006 [Details]
    2006 Problem Based Learning: A Software Engineering Curriculum Proposal
    J O’Kelly, R Monahan, J Gibson, S Brown (2006) Problem Based Learning: A Software Engineering Curriculum Proposal International Conference of Software Engineering [Details]
    2005 Software refinement with perfect developer
    Carter G.;Monahan R.;Morris J. (2005) Software refinement with perfect developer Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005 , pp.363-372 [DOI] [full-text] [Details]
    2005 Software Refinement with Perfect Developer
    Carter G, Monahan R, Morris J (2005) Software Refinement with Perfect Developer Software Engineering and Formal Methods, Koblenz, Germany, 7-9 September 2005 [full-text] [Details]
    2002 Reveal: A Tool to Reverse Engineer Class Diagrams
    Sarah Matzko and Peter J. Clarke and Tanton H. Gibbs and Brian A. Malloy and James F. Power and Rosemary Monahan (2002) Reveal: A Tool to Reverse Engineer Class Diagrams International Conference on Technology of Object-Oriented Languages and Systems Sydney, Australia, , pp.13-21 [Details]
    1997 Tactics for Transformational Programming
    Monahan, R. and Geiselbrechtinger, F. (1997) Tactics for Transformational Programming 1st Irish Workshop on Formal Methods:Electronic Workshops in Computing, July 1997 [full-text] [Details]

    Conference Contributions

      Year Publication
    2016 Evaluating SMT solvers for software verification.
    Andrew Healy and Rosemary Monahan and James F. Power (2016) Evaluating SMT solvers for software verification. [Non Refereed Paper/Abstract Presented at Conference], 32nd British Colloquium of Theoretical Computer Science, Belfast, Northern Ireland [Details]
    2016 A Logical Framework for Integrating Software Models via Refinement.
    Marie Farrell and Rosemary Monahan and James F. Power (2016) A Logical Framework for Integrating Software Models via Refinement. [Non Refereed Paper/Abstract Presented at Conference], 32nd British Colloquium of Theoretical Computer Science, Belfast, Northern Ireland , 22-MAR-16 - 24-MAR-16 [full-text] [Details]
    2016 Using the theory of institutions to integrate software models via refinement.
    Marie Farrell and Rosemary Monahan and James F. Power (2016) Using the theory of institutions to integrate software models via refinement. [Non Refereed Paper/Abstract Presented at Conference], PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications, Iceland [Details]
    2009 European conference on Object-Oriented Programming 2009.
    (2009) European conference on Object-Oriented Programming 2009. [Oral Presentation], Program verification using the Spec# Programming System, Genova, Italy [Details]
    2009 Microsoft Research Seminar.
    (2009) Microsoft Research Seminar. [Oral Presentation], VSI Benchmarks and their verification in Dafny, MDR Redmond, USA [Details]

    Book Review

      Year Publication
    2010 Test case generation for programming language metamodels.
    Hao Wu, Rosemary Monahan, and James F. Power. (2010) Test case generation for programming language metamodels. Book Review [full-text] [Details]

    Conference Paper

      Year Publication
    2013 Ars: Analogical Reasoning for reuse of Implementation & Specification.
    Pitu M, Grijincu D, Li P, Saleem A, Monahan R, O'Donoghue D.P (2013) Ars: Analogical Reasoning for reuse of Implementation & Specification. Conference Paper [full-text] [Details]
    2012 Case Based Specifications - reusing specifications, programs and proofs.
    Dr Rosemary Monahan, Dr Diarmuid O'Donoghue (2012) Case Based Specifications - reusing specifications, programs and proofs. Conference Paper [full-text] [Details]

    Editorial

      Year Publication
    2015 VerifyThis 2012 A Program Verification Competition.
    Huisman, M;Klebanov, V;Monahan, R (2015) VerifyThis 2012 A Program Verification Competition. HEIDELBERG: Editorial [DOI] [Details]
    2014 Evaluating Software Verification Systems: Benchmarks and Competitions.
    D Beyer, M Huisman, V Klebanov, R Monahan (2014) Evaluating Software Verification Systems: Benchmarks and Competitions. Editorial [full-text] [Details]

    Newspaper Articles

      Year Publication
    2014 An initiative to introduce Computational Thinking in to second level education.
    A Mooney, S Bergin, J Duffin, T Naughton, R Monahan, J Power, (2014) An initiative to introduce Computational Thinking in to second level education. Newspaper Articles [Details]

    Thesis

      Year Publication
    2009 Data Refinement in Object-Oriented Verification.
    Monahan, Rosemary (2009) Data Refinement in Object-Oriented Verification. Dublin City University: Thesis [Details]
    1998 Deduction Based Transformational Programming, MSc Thesis, Department of Computer Science, UCD, (February 1998).
    Monahan, Rosemary (1998) Deduction Based Transformational Programming, MSc Thesis, Department of Computer Science, UCD, (February 1998). University College Dublin: Thesis [Details]

    Technical Publication

      Year Publication
    2012 A simple complexity measurement for software verification and software testing.
    Cheng Z, Monahan R, and Power J.F.. (2012) A simple complexity measurement for software verification and software testing. Technical Publication [full-text] [Details]
    2005 Introducing the Perfect Language.
    Carter G, Monahan R (2005) Introducing the Perfect Language. Technical Publication [full-text] [Details]
    2005 Testing Guidelines for Student Projects.
    Brown S, Monahan R (2005) Testing Guidelines for Student Projects. Technical Publication [full-text] [Details]
    2005 Enhancing Skills Transfer through Problem Based Learning.
    OKelly J, Monahan R, Gibson P, Brown S (2005) Enhancing Skills Transfer through Problem Based Learning. Technical Publication [full-text] [Details]
    2005 Software Specification, Implementation and Execution with Perfect.
    Carter G, Monahan R (2005) Software Specification, Implementation and Execution with Perfect. Technical Publication [full-text] [Details]
    1997 Implementing Specifications by Transformational Programming.
    Monahan R, Geiselbrechtinger F (1997) Implementing Specifications by Transformational Programming. Technical Publication [Details]
    1997 Transformational Programming and Theorem Proving.
    Monahan R, Geiselbrechtinger F (1997) Transformational Programming and Theorem Proving. Technical Publication [Details]
    1996 Reification of Abstract Data Types using Monoid Homomorphisms.
    McLoughlin H, Monahan R (1996) Reification of Abstract Data Types using Monoid Homomorphisms. Technical Publication [Details]
    1996 Implementing Specifications by Transformational Programming.
    Monahan R, Geiselbrechtinger F (1996) Implementing Specifications by Transformational Programming. Technical Publication [Details]

    Professional Associations

      Association Function From / To
    European Joint Conferences on Theory and Practice of Software Member /
    Association for Computing Machinery Member /
    Irish ACM Special Interest Group on Computer Science Education Founding Member /
    Irish ACM-W chapter for Computer Science Founding Member /

    Committees

      Committee Function From / To
    Irish Workshop in Formal Methods Local Organisation Committee Member 1997 / 1997
    integrated Formal Methods Program Committee Co-chair 2022 /
    Curriculum Commission Working Group on Enhancing Teaching and Learning Computer Science Representative 2014 / 2015
    Equality, Diversity and Inclusion, Science and Engineering Faculty Committee Computer Science Representative 2021 /
    ICS Robocode Challenge MU Computer Science 2006 / 2012
    Irish Network for Gender Equality in Computing (INGENIC) MU representative 2017 / 2023
    Third-Level Computing Forum MU Computer Science 2021 /
    National University of Ireland Senate MU Academic representative 2007 / 2017
    Formal Techniques for Java-like Programs (FTfJP) Program Committee (Reviewer) 2009 /
    Formal Techniques for Java-like Programs (FTfJP) Program Committee (Reviewer) 2011 /
    European Summer School in Logic, Language and Information, Student session (ESSLLI STUS) Program Committee (Reviewer) 2017 /
    WORKSHOP ON ALGEBRAIC DEVELOPMENT TECHNIQUES (WADT) Program Committee (Reviewer) 2020 /
    Formal Methods (FM) Program Committee Reviewer 2021 /
    Formal Integrated Development Environment (F-IDE) Program Committee (Reviewer) 2021 /
    Formal Methods for Autonomous Systems (FMAS) Reviewer 2021 /
    Formal Methods for Autonomous Systems (FMAS) Program Committee (Reviewer) 2020 /
    ABZ: Rigorous State Based Methods Program Committee (Reviewer) 2020 /
    ABZ: Rigorous State Based Methods Program Committee (Reviewer) 2021 /
    Formal Techniques for Java-like Programs (FTfJP) Steering Committee Member 2015 / 2017
    Formal Techniques for Java-like Programs (FTfJP) Steering Committee Steering Committee Chair 2017 / 2023
    VerifyThis Steering Committee Steering Committee Member 2011 / 2023
    Formal Methods for Industrial Critical Systems (FMICS) Program Committee (Reviewer) 2022 /
    Capitation Committee (NUIM) MU Academic representative 2002 / 2014
    Innovation and Technology in Computer Science Education (ITiCSE) Local Organiser 2022 /
    China-Ireland Information and Communications Technologies Conference (CIICT) Program Committee (Reviewer) 2009 /
    Irish Conference on Engaging Pedagogy (ICEP) Program Committee (Reviewer) 2011 /
    Formal Verification of Object-Oriented Software (FoVeOOS) Program Committee (Reviewer) 2010 /
    Formal Verification of Object-Oriented Software (FoVeOOS) Program Committee (Reviewer) 2011 /
    COMPARE Program Committee (Reviewer) 2012 /
    Automated Software Engineering Tools (ASE Tools) Program Committee (Reviewer) 2013 /
    International Colloquium on Theoretical Aspects of Computing (ICTAC) Program Committee (Reviewer) 2014 /
    ACM/SIGAPP Symposium On Applied Computing (SAC) Program Committee (Reviewer) 2012 /
    ACM/SIGAPP Symposium On Applied Computing (SAC) Program Committee (Reviewer) 2013 /
    ACM/SIGAPP Symposium On Applied Computing (SAC) Program Committee (Reviewer) 2016 /
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Program Committee (Reviewer) 2018 /
    integrated Formal Methods (iFM) Program Committee (Reviewer) 2016 /
    integrated Formal Methods (iFM) Program Committee (Reviewer) 2017 /
    Formal Methods (FM) Program Committee (Reviewer) 2019 /
    Formal Techniques for Java-like Programs (FTfJP) Program Committee Chair 2015 /
    integrated Formal Methods (iFM) General Chair 2018 /
    Formal Integrated Development Environment (F-IDE) General Chair 2019 /
    Formal Integrated Development Environment (F-IDE) General Chair 2018 /
    Formal Methods for Industrial Critical Systems (FMICS) Local Organiser Chair 2018 /
    COST Action IC0701 European scientific cooperation management committee Irish representative 2008 / 2012
    Irish Workshop in Formal Methods Local Organisation Committee Member 2002 /
    Principles and Practice of Programming in Java Program Committee Member 2002 /
    Faculty of Science Human Resources Focus Group (NUIM) Member /
    Principles and Practice of Programming in Java Local Organisation Committee Member 2003 /
    Human Resources Committee (NUIM) Member 2000 / 2005
    Science of Computer Programming Editor/review 2022 /
    Student Affairs Committee (NUIM) Member 2000 / 2005
    Governing Authority of NUIM Academic Staff Representative 2000 / 2005

    Employment

      Employer Position From / To
    Maynooth University Associate Professor 01-OCT-16 /
    University College Dublin Research Assistant / 30-SEP-94
    Griffith College Dublin Lecturer / 01-SEP-99
    University College Dublin Occasional Lecturer / 01-JUN-99
    University College Dublin Course Administrator / 30-JUN-97
    NUI Maynooth Lecturer 01-OCT-99 / 30-SEP-16
    University College Dublin Assistant Lecturer / 01-SEP-98
    University College Dublin Tutor / 31-MAY-97

    Education

      Year Institution Qualification Subject
    1995 University College Dublin B.Sc.
    2010 Dublin City University PhD Computer Science
    1998 University College Dublin M.Sc.

    Reviews

      Journal Role
    Science Of Computer Programming Reviewer
    Journal Of Automated Reasoning Reviewer
    International Journal On Software Tools For Technology Transfer Guest Editor
    Ieee Intelligent Systems And Their Applications Reviewer
    International Journal On Software Tools For Technology Transfer Reviewer
    Formal Aspects Of Computing Reviewer

    Teaching Interests

    I currently teach research-led modules on Software Verification at 3rd year BSc level and Rigorous Software process at MSc Level.

    My research on techniques and tools for the development of dependable software feds directly into the classroom, so that students learn about current and evolving software verification techniques with hands-on experience of practical tools that we can use to develop reliable software. My teaching emphasises rigour and formality throughout the software development life-cycle, building on the foundations for reasoning about software correctness,  the underlying logics used, and demonstrating the state of the art techniques and tools. Current research developments and the usage of these techniques in industry is informed by existing research collaborations.

    Topics include Design by Contract; Logics such as Hoare Logic, Temporal Logic and Separation Logic; Specification Languages such as JML, Eiffel, Dafny and Event-B; as well as verification techniques and tools used for reasoning about program correctness including deductive verification, model checking, refinement and SMT solvers. 

    Recent Teaching Activities: Dept. of Computer Science, MU, Ireland
    • CS357 Software Verification (BSc Year 3)
    • CS424 Program Language Semantics (BSc Year 4)
    • CS431 Model Checking (BSc Year 4)
    • CS603/CS803 Rigorous Software Process (MSc/PhD)
    • CS613/CS813 Advanced Concepts in Object Oriented Programming (MSc/PhD)
    • CS629 Directed Reading (MSc)
    • CS640 MSc in Software Engineering Dissertations
    • CS645 Erasmus Mundus MSc in Dependable Software Systems (DESEM) : Co-ordination and Supervision
    • CS650/CS655 MSc DESEM International Summerschool (Organization of 2 week-long summerschool in Ireland 2013, Scotland 2014, France 2015).

    Teaching exchanges:
    • Université de Lorraine, France (MSc, Software Verification, 2011- 2015, 2018)
    • Zhejiang University, China (BSc2, Software Engineering, 2011)

    Previous Teaching Activities: Dept. of Computer Science, MU, Ireland
    • Introduction to Programming (BSc Year 1)
    • Algorithms and Data Structures 1 (BSc Year 2)
    • Algorithms and Data Structures 2 (BSc Year 2)
    • Software Engineering - Object-Oriented Design (BSc Year 2)
    • Software Engineering - Parallel Programming (BSc Year 2)
    • Discrete Structures (Arts Year 1, Computer Science & Software Engineering Year 1, Venture Management Year 1, BSc Year 1)
    • Z Specification & Program Verification (BSc Year 3 and BSc Year 4)
    • Denotational Semantics (BSc Year 4).

    Recent Postgraduates

      Graduation Student Name University Degree Thesis
    2006 Gareth Carter Maynooth University MSc Support tools for Object Oriented Software Development
    2015 Jagadeeswaran Thangaraj Maynooth University MSc Adding Ownership Constraints to OCL
    2016 Keith Dooley Maynooth University MSc A MDE approach for Refactoring Software Systems
    2017 Marie Farrell Maynooth University Doctor of Philosophy Event-B in the Institutional Framework: Defining a Semantics, Modularisation Constructs and Interoperability for a Specification Language
    2013 Hao Wu Maynooth University Doctor of Philosophy Automated Metamodel Instance Generation Satisfying Quantitative Constraints
    2016 Zheng Cheng Maynooth University Doctor of Philosophy Formal Verification of Relational Model Transformations using an Intermediate Verification Language
    2016 Andrew Healy Maynooth University MSc Predicting SMT solver performance for software verification

    External Collaborators

      Name Role / Description Country
    Dr Rustan Leino. Amazon AWS Research in Software Engineering and Program Verification U.S.A.
    Prof. Dr. Peter Müller / ETH Zurich VerifyThis Verification Competitions SWITZERLAND
    Dr. Mattias Ulbrich / KIT VerifyThis Verification Competitions GERMANY
    Dr. Bernhard Beckert, Karlsruhe Institute of Technology Cost Action IC0701 GERMANY
    Prof Joseph Morris. Dublin City University PhD Research IRELAND
    Dr. Georgios Giantamidis, United Technologies Research Center Aircraft Engine Controller verification IRELAND
    Dr Marieke Huisman. University of Twente VerifyThis Verification Competitions NETHERLANDS
    Prof Dominique Mery, INRIA, UL and LORIA Research on Modeling languages and specification e.g. Event B, Spec# FRANCE
    Dr. Stylianos (Stelios) Basagiannis, United Technologies Research Centre Aircraft Engine Controller verification IRELAND