Prof Rosemary Monahan

    Computer Science, Hamilton Institute

    Gaeilge agus fáilte

    Professor

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

    Biography

    Rosemary Monahan is a 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, a PhD from DCU and is the Maynooth University institutional lead for ADAPT, the SFI Research Centre for AI-Driven Digital Content Technology.

    As a founding member of the Principles of Programming Research Group she specialises in the static and dynamic analysis of software. She has expertise in the modelling, analysis and verification of software, 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). 

    Professor 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 a Principal Investigator (PI) under the Science Foundation Ireland Frontiers for the Future Programme, working on verification and visualisation of AI based-systems (MAIVV, 2021-2025), and a Funded Investigator (FI) working on VERIFAI: Traceability and Verification of Natural LAnguage Requirements in ADAPT, the SFI Research Centre for AI-Driven Digital Content Technology.

    Recent projects include research funded by Enterprise Ireland and H2020 ESCEL JU programme to improve workflows and tools for verification and validation of software systems (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.

    Professor Monahan has been PI on two SFI Discover projects (InSPECT 2019-2022; CoCoA 2021-2023) producing educational resources that teach the science of problem-solving through computational thinking and she is currently a funded collaborator on CoCoA23 (2023 - 2025) improving scientific problem solving skills through co-creation, collaboration and active learning. 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.

    External PhD Examination

    • Generation automatique d'obligations de preuves parametree pas des theories de domaine dans Event-B: La care de travail EB4EB, Peter Riviere, Universite de Toulouse, France, 2024
    • Exploring Annotations for Deductive Verification, Sophie Lathouwers, University of Twente, The Netherlands, 2023
    • Efficient Techniques and Tools for Software Testing Based on Traces and Coverage Analysis, Faustin Ahishakiye, Western Norway University of Applied Sciences, Norway, 2022
    • Towards a practically extensible Event-B methodology, Issam Maamria, University of Southampton, UK, 2012

    .

    Research Projects

    Title Role Description Start date End date Amount
    MAIVV: Modular AI Verification and Visualisation PI 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/12/2021 30/11/2025 620826.6
    TechMate A best practice toolkit for driving sustainable acceleration towards gender equality in technology disciplines in HEIs Collaborator This partnership of Higher Education Institutes (HEIs) and the HEA designs and develops a toolkit of best practice for recruitment and retention of female university students in technology. Lead partners are TU Dublin, MU, IT Carlow and UCD. Funded by the HEA Gender Equality Enhancement Fund. 01/01/2021 31/12/2021 33000
    INGENIC: Irish Network for Gender Equality in Computing Collaborator This partnership of Irish HEIs and the HEA co-ordinates efforts to address the under-representation of females in Computer Science. Lead partners are IADT, MU and GMIT, supported by members of the INGENIC network. Funded by the HEA Gender Equality Enhancement Fund. 01/01/2021 31/12/2021 23800
    CoCoA: Co-create Collaborate Activate - Advancing Computational Thinking Education PI 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/01/2021 31/12/2022 149375.77
    VALU3S - Verification and Validation of Automated Systems' Safety and Security (Stage 2) PI 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/05/2020 30/04/2023 0
    InSPECT: Introducing the Science of Problem-solving through Education in Computational Thinking PI 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/01/2019 31/12/2021 272895
    A constructive framework for software specification and refinement in Event-B / Conor Reynolds PI 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/09/2019 31/08/2023 105333.12
    Building Reliable Software Systems – Software Refinement meets Software Verification PI 01/01/2013 31/12/2013 0
    Request for travel fund for a workshop, May 6 – 9 2014, Lorenz Center, Leiden, The Netherlands PI 06/05/2014 09/05/2014 0
    A Logical Framework for Integrating Software Models via Refinement. PI 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/10/2013 30/09/2017 95680
    FMICS/iFM 2018 PI 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/08/2018 07/09/2018 10370
    FMICS/iFM 2018 Conferences PI FMICS/iFM are conference that I will host at MU from Sept 3rd - 7th. 03/09/2018 07/09/2018 1400

    Post Doctoral Fellows / Research Team

    Researcher Name Project Funding Body
    Dara John Dillon Andrea Mac Conville Verification of Robotic Systems
    Taina Marja Lehtimaki CoCoA:Co-create, Collaborate Activate – Advancing Computational Thinking Education
    Taina Marja Lehtimaki InSPECT: Introducing the Science of Problem-solving through Education in Computational Thinking
    Jonathan Mark Lambert A Multi-dimensional Model of Interpreted Language Power Consumption
    Oisin Sheridan VALU3S: Verification and Validation of Automated Systems’ Safety and Security
    Conor Reynolds A constructive framework for software specification and refinement in Event-B

    Edited Book

    Year Publication
    2022 Maurice H. ter Beek, ISTI-CNR, Pisa, Italy;Rosemary Monahan, Maynooth University, Maynooth, Ireland (Ed.). (2022) Integrated Formal Methods 2022. Europe, the USA, and Asia: Springer Nature, [Link]

    Peer Reviewed Journal

    Year Publication
    2024 Reynolds, C.; Monahan, R. (2024) 'Reasoning about logical systems in the Coq proof assistant'. Science of Computer Programming, 233 . [Link] [DOI]
    2023 MacConville, D.; Farrell, M.; Luckcuck, M.; Monahan, R. (2023) 'CSP2Turtle: Verified Turtle Robot Plans †'. Robotics, 12 . [Link] [DOI]
    2023 Inkarbekov, M.; Monahan, R.; Pearlmutter, B.A. (2023) 'Visualization of AI Systems in Virtual Reality: A Comprehensive Review'. International Journal of Advanced Computer Science and Applications, 14 . [Link] [DOI]
    2022 Farrell M.; Monahan R.; Power J.F. (2022) 'BUILDING SPECIFICATIONS IN THE EVENT-B INSTITUTION'. Logical Methods in Computer Science, 18 (4):4:1-4:55. [DOI] [Full-Text]
    2022 Lambert J.; Monahan R.; Casey K. (2022) 'Accidental Choices—How JVM Choice and Associated Build Tools Affect Interpreter Performance'. Journal of Computers, 11 (6). [DOI]
    2021 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] [Full-Text]
    2021 Farrell, Marie and Monahan, Rosemary and Power, James F (2021) 'Building Specifications in the Event-B Institution'. . [Full-Text]
    2021 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'. 10 (7). [Link] [DOI] [Full-Text]
    2017 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]
    2017 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]
    2016 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]
    2015 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]

    Conference Publication

    Year Publication
    2023 Farrell, M.; Monahan, R.; Power, J.F. (2023) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Building Specifications in the Event-B Institution: A Summary [Link] [DOI]
    2023 Flinkow, T.; Pearlmutter, B.A.; Monahan, R. (2023) Proceedings - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2023 Rich and Expressive Specification of Continuous-Learning Cyber-Physical Systems [Link] [DOI]
    2023 Flinkow, T.; Pearlmutter, B.A.; Monahan, R. (2023) Electronic Proceedings in Theoretical Computer Science, EPTCS Comparing Differentiable Logics for Learning Systems: A Research Preview [Link] [DOI]
    2023 Lehtimäki, T.; Monahan, R.; Mooney, A.; Casey, K.; Naughton, T.J. (2023) Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE Computational Thinking Resources Inspired by Bebras [Link] [DOI]
    2023 Lehtimäki, T.; Monahan, R.; Mooney, A.; Casey, K.; Naughton, T.J. (2023) Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE A Computational Thinking Obstacle Course Based on Bebras Tasks for K-12 Schools [Link] [DOI]
    2022 Reynolds C.; Monahan R. (2022) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Machine-Assisted Proofs for Institutions in Coq [DOI]
    2022 Lehtimäki T.; Hamm J.; Mooney A.; Casey K.; Monahan R.; Naughton T.J. (2022) ACM International Conference Proceeding Series A computational thinking module for secondary students and pre-service teachers using Bebras-style tasks [DOI]
    2022 Farrell M.; Luckcuck M.; Sheridan O.; Monahan R. (2022) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Towards Refactoring FRETish Requirements [DOI]
    2022 Luckcuck M.; Farrell M.; Sheridan O.; Monahan R. (2022) IEEE Aerospace Conference Proceedings A Methodology for Developing a Verifiable Aircraft Engine Controller from Formal Requirements [DOI]
    2022 Lehtimäki T.; Monahan R.; Mooney A.; Casey K.; Naughton T.J. (2022) Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE Bebras-inspired Computational Thinking Primary School Resources Co-created by Computer Science Academics and Teachers [DOI]
    2022 MacConville D.; Farrell M.; Luckcuck M.; Monahan R. (2022) Electronic Proceedings in Theoretical Computer Science, EPTCS Modelling the Turtle Python library in CSP [DOI]
    2022 Farrell M.; Luckcuck M.; Sheridan O.; Monahan R. (2022) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller [DOI]
    2022 Sheridan O.; Monahan R.; Luckcuck M. (2022) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) A Requirements-Driven Methodology: Formal Modelling and Verification of an Aircraft Engine Controller [DOI]
    2021 Aiyankovil, K.G.; O’Donoghue, D.P.; Monahan, R. (2021) Proceedings of the 12th International Conference on Computational Creativity, ICCC 2021 Creating new Program Proofs by Combining Abductive and Deductive Reasoning [Link]
    2021 Aiyankovil K.G.; Monahan R.; O’Donoghue D.P. (2021) CEUR Workshop Proceedings Upcycling formal specifications for similar implementations with Arís [Full-Text]
    2021 Farrell M.; Reynolds C.; Monahan R. (2021) FTfJP 2021 - Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, co-located with ECOOP/ISSTA 2021 Using dafny to solve the VerifyThis 2021 challenges [DOI] [Full-Text]
    2018 Marie Farrell and Rosemary Monahan and James F. Power and Michael Fisher (2018) 24th International Workshop on Algebraic Development Technique An Approach to Combining the Institutions for Event-B and Temporal Logic Royal Holloway University of London, [Link] [Full-Text]
    2018 Masci, P; Monahan, R; Prevosto, V (2018) ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE Proceedings 4th Workshop on Formal Integrated Development Environment Oxford, England, 14 July 2018 Preface
    2017 Marie Farrell and Rosemary Monahan and James F. Power (2017) International Conference on Software Engineering and Formal Methods Specification Clones: An Empirical Study of the Structure of Event-B Specifications Trento, Italy, 04/09/2017- 08/09/2017 [DOI] [Full-Text]
    2017 Farrell M.; Monahan R.; Power J. (2017) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) An Institution for Event-B [DOI]
    2017 Marie Farrell, Rosemary Monahan and James F. Power (2017) International Conference on Formal Engineering Methods Combining Event-B and CSP: An institution theoretic approach to interoperability Xi'an, China, 13/11/2017- 17/11/2017 [DOI] [Full-Text]
    2017 Marie Farrell and Rosemary Monahan and James F. Power (2017) Recent Trends in Algebraic Development Techniques An Institution for Event-B [Full-Text]
    2016 Cheng, Z; Mery, D; Monahan, R (2016) LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I On Two Friends for Getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in RODIN [DOI] [Full-Text]
    2016 Andrew Healy and Rosemary Monahan and James F. Power (2016) 31st ACM Symposium on Applied Computing Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving Pisa, Italy, [DOI] [Full-Text]
    2016 Andrew Healy, Rosemary Monahan, and James F. Power. (2016) 3rd Workshop on Formal Integrated Development Environment Predicting SMT solver performance for software verification Limassol, Cyprus, [DOI] [Full-Text]
    2016 Farrell, Marie and Monahan, Rosemary and Power, James F (2016) International Workshop on Algebraic Development Techniques An institution for Event-B
    2015 Cheng, Z; Monahan, R; Power, JF (2015) 8th INTERNATIONAL CONFERENCE ON THEORY AND PRACTICE OF MODEL TRANSFORMATIONS A Sound Execution Semantics for ATL via Translation Validation Research Paper [DOI] [Full-Text]
    2015 Zheng Cheng and Rosemary Monahan and James F. Power (2015) 4th International Workshop on the Verification Of Model Transformations Verifying SimpleGT Transformations Using an Intermediate Verification Language L'Aquila, Italy, [Link] [Full-Text]
    2014 Aidan Mooney and Joseph Duffin and Thomas Naughton and Rosemary Monahan and James Power and Phil Maguire (2014) International Conference on Engaging Pedagogy PACT: An initiative to introduce Computational Thinking in to second level education Athlone, Ireland, [Link]
    2014 Mooney, Aidan; Duffin, Joe; Naughton, Thomas J; Monahan, Rosemary; Power, James F; Maguire, Phil (2014) ICEP 2014 PACT: An initiative to introduce computational thinking to second-level education in Ireland
    2014 D P ODonoghue, R Monahan, D Grijincu, M Pitu, F. Halim, F Rahman, Y Abgaz, D Hurley (2014) C3GI 2014 Creating Formal Specifications with Analogical Reasoning [Full-Text]
    2013 Wu, H; Monahan, R; Power, JF (2013) 2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE) Exploiting attributed type graphs to generate metamodel instances using an SMT solver [DOI] [Full-Text]
    2013 Dr Rosemary Monahan, Prof Dominique Mery (2013) Verification and Program Transformation 2013 Transforming Event B Models into Verified C# Implementations [Full-Text]
    2012 Huisman Marieke, Vladimir Klebanov, Rosemary Monahan (2012) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems On the Organisation of Program Verification Competitions [Full-Text]
    2012 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) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) The COST IC0701 verification competition 2011 [DOI] [Full-Text]
    2012 Monahan, Dr Rosemary Zheng Cheng, Dr James F. Power (2012) Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012) A Simple Complexity Measurement for Software Verification and Software Testing 28-31 [Full-Text]
    2011 Monahan Rosemary, Zheng Cheng, Aidan Mooney (2011) ICEP 2011 nExaminer: A Semi-automated Computer Programming Assignment Assessment Framework for Moodle [Full-Text]
    2011 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) Formal Methods 2011 The 1st Verified Software Competition, Extended Experience Report. [Full-Text]
    2023 Inkarbekov, M.; Pearlmutter, B.A.; Monahan, R. (2023) Immersive Neural Network Exploration: A VR Approach to Human-Centered AI Understanding [Link] [DOI]
    2010 Monahan Rosemary, Power James, Wu Hao (2010) 2nd International Workshop on Model Transformation with ATL (MtATL 2010) Using ATL in a tool-chain to calculate coverage data for UML class diagrams [Full-Text]
    2010 Monahan, Rosemary; Xu Yan (2010) CIICT 2010 Implementing the Verified Software Initiative Benchmarks using Perfect Developer [Full-Text]
    2010 Leino K.; Monahan R. (2010) Lecture Notes in Computer Science. Proceedings of VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS Dafny meets the verification benchmarks challenge [DOI]
    2010 Leino, K. Rustan M. and Monahan, Rosemary (2010) 13th Brazilian Symposium on Formal Methods (SBMF 2010), Brazil 2010 Using Boogie 2 in the Verification of Spec# Programs
    2010 Wu H.; Monahan R.; Power J. (2010) CEUR Workshop Proceedings Using ATL in a tool-chain to calculate coverage data for UML class diagrams [Full-Text]
    2009 Leino, K. Rustan M. and Monahan, Rosemary (2009) ECOOP (Summerschool, 9th July 2009, Genoa, Italy) Program Verification Using the Spec# Programming System
    2009 Leino, K. Rustan M. and Monahan, Rosemary (2009) 24th Annual ACM Symposium on Applied Computing Reasoning about Comprehensions with First-Order SMT Solvers [Full-Text]
    2008 Leino, K. Rustan M. and Monahan, Rosemary (2008) ETAPS (Spec# Tutorial, Budapest, Hungary, March 2008) Program Verification Using the Spec# Programming System
    2007 Leino, K. Rustan M. and Monahan, Rosemary (2007) Formal Techniques for Java-Like Programs, ECOOP Workshop, Berlin, Germany, July 2007 Automatic verification of textbook programs that use comprehensions [Full-Text]
    2006 Parham J.R., O' Kelly J., Monahan R., Stevenson D.E. (2006) International Conference on Frontiers in Education: Computer Science and Computer Engineering, Las Vegas, USA, 26-29 June 2006 The Relevance of Scientific Reasoning Skills to Computer Science: A Comparative Study between the US and Ireland
    2006 J O’Kelly, R Monahan, J Gibson, S Brown (2006) International Conference of Software Engineering Problem Based Learning: A Software Engineering Curriculum Proposal
    2005 Carter G.; Monahan R.; Morris J. (2005) Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005 Software refinement with perfect developer [DOI] [Full-Text]
    2005 Carter G, Monahan R, Morris J (2005) Software Engineering and Formal Methods, Koblenz, Germany, 7-9 September 2005 Software Refinement with Perfect Developer [Full-Text]
    2002 Sarah Matzko and Peter J. Clarke and Tanton H. Gibbs and Brian A. Malloy and James F. Power and Rosemary Monahan (2002) International Conference on Technology of Object-Oriented Languages and Systems Reveal: A Tool to Reverse Engineer Class Diagrams Sydney, Australia, [Link]
    1997 Monahan, R. and Geiselbrechtinger, F. (1997) 1st Irish Workshop on Formal Methods:Electronic Workshops in Computing, July 1997 Tactics for Transformational Programming [Full-Text]

    Other Journal

    Year Publication
    2022 Marie Farrell and Matt Luckcuck and Oisin Sheridan and Rosemary Monahan (2022) 'Towards Refactoring FRETish Requirements' arXiv:2201.04531 [cs.SE], .
    2022 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], .
    2021 Marie Farrell and Rosemary Monahan and James F. Power (2021) 'Building Specifications in the Event-B Institution' Jacobin, . [Link] [Full-Text]
    2021 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], . [Full-Text]
    2021 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], .
    2019 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]
    2018 Masci P.; Monahan R.; Prevosto V. (2018) 'Proceedings 4th Workshop on Formal Integrated Development Environment' Electronic Proceedings in Theoretical Computer Science, EPTCS, 284 . [DOI]
    2012 Hao Wu and Rosemary Monahan and James F. Power (2012) 'Metamodel Instance Generation: A systematic literature review' arXiv:1211.6322 [cs.SE], . [Full-Text]

    Editorial

    Year Publication
    2022 Ter Beek M.H.; Monahan R. (2022) Preface. [Editorial]
    2015 Huisman, M; Klebanov, V; Monahan, R (2015) VerifyThis 2012 A Program Verification Competition. HEIDELBERG: [Editorial] [DOI]
    2014 D Beyer, M Huisman, V Klebanov, R Monahan (2014) Evaluating Software Verification Systems: Benchmarks and Competitions. [Editorial] [Full-Text]

    Book Chapter

    Year Publication
    2015 Dr Rosemary Monahan (2015) 'A Sound Execution Semantics for ATL via Translation Validation' In: Kolovos, Dimitris; Manuel, Wimmer(Eds.). Theory and Practice of Model Transformations . L'Aquila, Italy : Springer. [Full-Text]

    Conference Paper

    Year Publication
    2013 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]
    2012 Dr Rosemary Monahan, Dr Diarmuid O'Donoghue (2012) Case Based Specifications - reusing specifications, programs and proofs. [Conference Paper] [Full-Text]

    Conference Contribution

    Year Publication
    2016 Andrew Healy and Rosemary Monahan and James F. Power (2016) 32nd British Colloquium of Theoretical Computer Science Evaluating SMT solvers for software verification Belfast, Northern Ireland, .
    2016 Marie Farrell and Rosemary Monahan and James F. Power (2016) 32nd British Colloquium of Theoretical Computer Science A Logical Framework for Integrating Software Models via Refinement Belfast, Northern Ireland, 22/03/2016-24/03/2016. [Full-Text]
    2016 Marie Farrell and Rosemary Monahan and James F. Power (2016) PhD Symposium at iFM'16 on Formal Methods: Algorithms, Tools and Applications Using the theory of institutions to integrate software models via refinement Iceland, .
    2009 (2009) Program verification using the Spec# Programming System European conference on Object-Oriented Programming 2009 Genova, Italy, .
    2009 (2009) VSI Benchmarks and their verification in Dafny Microsoft Research Seminar MDR Redmond, USA, .
    2012 Monahan, R. O'Donoghue D.P. (2012) Case Based Specifications: Re-using programs, specifications and proofs Schloss Dagstuhl - Leibniz Center for Informatics Germany, .
    2010 Hao Wu and Rosemary Monahan and James F. Power (2010) Doctoral Symposium of the 3rd International Conference on Software Language Engineering Test case generation for programming language metamodels Eindhoven, Netherlands, .

    Book Review

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

    Newspaper Articles

    Year Publication
    2014 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]

    Thesis

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

    Technical Publication

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

    Other Publication

    Year Publication
    2022 Ter Beek, M.H.; Monahan, R. (2022) Preface. [Link]
    2019 Huisman, Marieke and Monahan, Rosemary and M\"uller, Peter and Paskevich, Andrei and Ernst, Gidon (2019) VerifyThis 2018: A Program Verification Competition.
    2017 Huisman, Marieke and Monahan, Rosemary and Müller, Peter and Mostowski, Wojciech and Ulbrich, Mattias (2017) VerifyThis 2017 : A Program Verification Competition.
    2016 Gurov, D; Havelund, K; Huisman, M; Monahan, R (2016) LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I. CHAM: [DOI]
    2012 Hao Wu and Rosemary Monahan and James F. Power (2012) Metamodel Instance Generation: A systematic literature review. [Full-Text]
    2009 (2009) Teaching Formal Methods.
    2009 (2009) Verified Software Initiative Benchmarks in Dafny.
    2009 (2009) A Spec# Overview.
    2009 (2009) Object-Oriented Data Refinement.
    2009 (2009) of Programming Research at NUIM.
    2009 Dominique Mery (2009) Erasmus Teaching Exchange: Lectures to MSc Computer Science students on Event B and Rodin platform.
    2009 (2009) Program Verification using Spec#.
    2009 (2009) The Spec# Programming System.
    2009 (2009) Data Refinement in Object-oriented.
    2009 Dominique Mery (2009) Departmental Seminar on Case studies in Event B.
    2023 Monahan, R.; Ter Beek, M.H. (2023) Introduction to the Special Collection from iFM 2022. [Link] [DOI]
    Certain data included herein are derived from the © Web of Science (2024) of Clarivate. All rights reserved.

    Professional Associations

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

    Employment

    Employer Position From / To
    Maynooth University Associate Professor 01/10/2016 -
    University College Dublin Research Assistant - 30/09/1994
    Griffith College Dublin Lecturer - 01/09/1999
    University College Dublin Occasional Lecturer - 01/06/1999
    University College Dublin Course Administrator - 30/06/1997
    NUI Maynooth Lecturer 01/10/1999 - 30/09/2016
    University College Dublin Assistant Lecturer - 01/09/1998
    University College Dublin Tutor - 31/05/1997
    Maynooth University Professor 01/10/2022 -

    Education

    Start date Institution Qualification Subject
    University College Dublin B.Sc.
    Dublin City University PhD Computer Science
    University College Dublin M.Sc.

    Editorial / Academic Reviews

    Amount Role From / To
    International Journal on Software Tools for Technology Transfer Guest Editor -
    Science of Computer Programming Reviewer -
    IEEE Intelligent Systems and Their Applications Reviewer -
    Science of Computer Programming Member of the Editorial Board 01/11/2022 - 01/11/2024
    Formal Aspects of Computing Reviewer -
    Journal of Automated Reasoning Reviewer -
    International Journal on Software Tools for Technology Transfer 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 Students

    Graduation date Name Degree
    2006 Gareth Carter MSc
    2015 Jagadeeswaran Thangaraj MSc
    2016 Keith Dooley MSc
    2017 Marie Farrell Doctor of Philosophy
    2013 Hao Wu Doctor of Philosophy
    2016 Zheng Cheng Doctor of Philosophy
    2016 Andrew Healy MSc

    External Collaborators

    Name Role Country
    Prof Dominique Mery, INRIA, UL and LORIA Research on Modeling languages and specification e.g. Event B, Spec# France
    Dr. Marie Farrell, University of Manchester Research collaboration United Kingdom
    Prof. Dr. Peter Müller / ETH Zurich VerifyThis Verification Competitions Switzerland
    Dr. Matthew Luckcuck, University of Derby Research collaboration United Kingdom
    Prof Joseph Morris. Dublin City University PhD Research Ireland
    Dr Marieke Huisman. University of Twente VerifyThis Verification Competitions Netherlands
    Dr. Stylianos (Stelios) Basagiannis, United Technologies Research Centre Aircraft Engine Controller verification Ireland
    Dr. Mattias Ulbrich / KIT VerifyThis Verification Competitions Germany
    Dr. Bernhard Beckert, Karlsruhe Institute of Technology Cost Action IC0701 Germany
    Dr Rustan Leino. Amazon AWS Research in Software Engineering and Program Verification United States
    Dr. Georgios Giantamidis, United Technologies Research Center Aircraft Engine Controller verification Ireland