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 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 PI on two SFI Discover projects which produce educational resources that teach the science of problem-solving through computational thinking (InSPECT, 2019-2021) and (CoCoA, 2020-2021). 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. 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.

    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 (€)
    CoCoA: Co-create Collaborate Activate - Advancing Computational Thinking Education PI Science Foundation Ireland / Discover Programme A follow on project to our SFI Discover 2018 project InSPECT which develops Computational Teaching resources for teachers, our team aims to develop teaching resources that develop skills in co-creation, communication and collaboration. 01-JAN-21 31-DEC-22 149375.77
    Introducing the Science of Problem-solving through Education in Computational Thinking PI Science Foundation Ireland / Discover Programme Our team will combine their prior experience in liaising with schools with their expertise in Computational Thinking pedagogy (in particular Bebras problems) to build relationships with disadvantaged DEIS schools in the SFI prioritised areas. The team will then exploit these relationships to engage our target audience with CT through teaching resources (lesson plans, workbooks, teacher portal) building upon carefully curated Bebras problems, and activities (workshops, school visits, and regional meetups). This will result in increased teacher, student, and parent interest and a corresponding enhanced involvement in STEM subjects. 01-JAN-19 31-DEC-20 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 thatmeets formal specifications, thus enhancing its reliability. The theory of institutions offers the unification of MDE with verification, and ensures consistency between different software models. Institutions are based on category theory, have deep roots in a well-developed branch of algebraic specification. 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. The proposed 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 will build 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 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

    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 '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] [Details]
    2018 'Formalised EMFTVM bytecode language for sound verification of model transformations'
    Zheng Cheng and Rosemary Monahan and James F. Power (2018) 'Formalised EMFTVM bytecode language for sound verification of model transformations'. Journal of Software and Systems Modeling, 17 (4):1197-1225 [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
    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]
    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
    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]
    2015 A sound execution semantics for ATL via translation validation
    Zheng Cheng, Rosemary Monahan, and James F. Power (2015) A sound execution semantics for ATL via translation validation 8th International Conference on Model Transformation L'Aquila, Italy, , pp.133-148 [DOI] [full-text] [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 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 Static and Runtime Verification, Competitors or Friends? (Track Summary)
    Gurov, D;Havelund, K;Huisman, M;Monahan, R (2016) Static and Runtime Verification, Competitors or Friends? (Track Summary) LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I , pp.397-401 [DOI] [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] [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 On two Friends for getting Correct Programs
    M\'ery, Dominique and Monahan, Rosemary and Zheng, Cheng (2016) On two Friends for getting Correct Programs . In: Bernhard Steffen and Tiziana Margaria eds. ISOLA 2016 CORFU, Greece, [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 Verifying simplegt transformations using an intermediate verification language
    Cheng Z.;Monahan R.;Power J. (2015) Verifying simplegt transformations using an intermediate verification language CEUR Workshop Proceedings , pp.12-19 [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 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 Exploiting attributed type graphs to generate metamodel instances using an SMT solver
    Wu H.;Monahan R.;Power J. (2013) Exploiting attributed type graphs to generate metamodel instances using an SMT solver International Symposium on Theoretical Aspects of Software Engineering , 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]
    2013 Exploiting attributed type graphs to generate metamodel instances using an SMT solver. To appear
    H. Wu, R. Monahan and J. F. Power (2013) Exploiting attributed type graphs to generate metamodel instances using an SMT solver. To appear TASE 2013 [full-text] [Details]
    2013 Exploiting attributed type graphs to generate metamodel instances using an SMT solver
    Hao Wu and Rosemary Monahan and James F. Power (2013) Exploiting attributed type graphs to generate metamodel instances using an SMT solver 7th International Symposium on Theoretical Aspects of Software Engineering , pp.175-182 [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 A Simple Complexity Measurement for Software Verification and Software Testing
    Zheng Cheng and Rosemary Monahan and James F. Power (2012) A Simple Complexity Measurement for Software Verification and Software Testing International Workshop on Comparative Empirical Evaluation of Reasoning Systems Manchester, UK, , pp.28-31 [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] [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]
    2012 On the organisation of program verification competitions
    Huisman M.;Klebanov V.;Monahan R. (2012) On the organisation of program verification competitions CEUR Workshop Proceedings , pp.50-59 [Details]
    2012 A simple complexity measurement for software verification and software testing - Discussion paper
    Cheng Z.;Monahan R.;Power J. (2012) A simple complexity measurement for software verification and software testing - Discussion paper CEUR Workshop Proceedings , 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 Test case generation for programming language metamodels
    Hao Wu and Rosemary Monahan and James F. Power (2010) Test case generation for programming language metamodels Doctoral Symposium of the 3rd International Conference on Software Language Engineering Eindhoven, Netherlands, [Details]
    2010 Dafny Meets the Verification Benchmarks Challenge
    Leino, KRM;Monahan, R (2010) Dafny Meets the Verification Benchmarks Challenge VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS [Details]
    2010 Using ATL in a tool-chain to calculate coverage data for UML class diagrams
    Hao Wu and Rosemary Monahan and James F. Power (2010) Using ATL in a tool-chain to calculate coverage data for UML class diagrams 2nd International Workshop on Model Transformation with ATL Malaga, Spain, , pp.60-64 [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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , pp.112-126 [DOI] [Details]
    2010 Program Verification
    Monahan, Rosemary (2010) Program Verification Integrated Formal Methods 2010 [Details]
    2010 Dafny meets the Benchmark Challenges
    Leino, K. Rustan M. and Monahan, Rosemary (2010) Dafny meets the Benchmark Challenges VSTTE [full-text] [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]
    2010 Est case generation for programming language metamodels: Abstract for software language engineering 2010 doctoral symposium
    Wu H.;Monahan R.;Power J. (2010) Est case generation for programming language metamodels: Abstract for software language engineering 2010 doctoral symposium CEUR Workshop Proceedings , pp.27-30 [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.;Monahan R. (2009) Reasoning about comprehensions with first-order SMT solvers Proceedings of the ACM Symposium on Applied Computing , pp.615-622 [DOI] [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]
    2005 Software refinement with perfect developer
    Carter, G;Monahan, R;Morris, JM (2005) Software refinement with perfect developer SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings , pp.363-372 [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]
    2002 Reveal: A tool to Reverse Engineer Class Diagrams
    Matzko S, Clarke P, Gibbs T, Malloy B, Power J, Monahan R (2002) Reveal: A tool to Reverse Engineer Class Diagrams Technology of Object-Orientated Languages and System, February 2002 [full-text] [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 COST Action Meeting, FM Week 2009.
    (2009) COST Action Meeting, FM Week 2009. [Oral Presentation], of Programming Research at NUIM, Eindhoven, Netherlands [Details]
    2009 COST Action Meeting, FM Week 2009.
    (2009) COST Action Meeting, FM Week 2009. [Oral Presentation], Teaching Formal Methods, Eindhoven, Netherlands [Details]
    2009 The Jave Modeling Language (JML) Dagstuhl.
    (2009) The Jave Modeling Language (JML) Dagstuhl. [Oral Presentation], The Spec# Programming System, Dagstuhl, Germany [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 LORIA Seminar Series.
    (2009) LORIA Seminar Series. [Oral Presentation], Program Verification using Spec#, Nancy, France [Details]
    2009 NUIM Comnputer Science Staff Seminar Series.
    (2009) NUIM Comnputer Science Staff Seminar Series. [Oral Presentation], A Spec# Overview, NUI Maynooth [Details]
    2009
    Dominique Mery (2009) [Visiting and guest lecturers hosted], Departmental Seminar on Case studies in Event B, UHP, Henri Poincaré University, Nancy, France, Science and Engineering, Computer Science [Details]
    2009
    Dominique Mery (2009) [Visiting and guest lecturers hosted], Erasmus Teaching Exchange: Lectures to MSc Computer Science students on Event B and Rodin platform, UHP, Henri Poincaré University, Nancy, France, Science and Engineering, Computer Science [Details]
    2009 COST Action Meeting, FM Week 2009.
    (2009) COST Action Meeting, FM Week 2009. [Oral Presentation], Object-Oriented Data Refinement, Eindhoven, Netherlands [Details]
    2009 JML Spec-a thon 2009.
    (2009) JML Spec-a thon 2009. [Oral Presentation], Verified Software Initiative Benchmarks in Dafny, University College Dublin [Details]
    2009 Microsoft Research Seminar.
    (2009) Microsoft Research Seminar. [Oral Presentation], VSI Benchmarks and their verification in Dafny, MDR Redmond, USA [Details]
    2009 PhD Viva.
    (2009) PhD Viva. [Oral Presentation], Data Refinement in Object-oriented, Dublin City University [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
    2019 Preface.
    Monahan R.;Prevosto V.;Proença J. (2019) Preface. Editorial [DOI] [Details]
    2018 Preface.
    Masci P.;Monahan R.;Prevosto V. (2018) Preface. Editorial [DOI] [Details]
    2015 VerifyThis 2012 A Program Verification Competition.
    Huisman, M;Klebanov, V;Monahan, R (2015) VerifyThis 2012 A Program Verification Competition. HEIDELBERG: Editorial [DOI] [Details]
    2015 Foreword.
    Monahan R. (2015) Foreword. Editorial [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]

    Committees

      Committee Function From / To
    Irish Workshop in Formal Methods Local Organisation Committee Member 1997 /
    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 /
    4th Irish Workshop on Formal Methods Local Organisation Committee Member /
    Student Affairs Committee (NUIM) Member /
    Governing Authority of NUIM Academic Staff Representative /

    Employment

      Employer Position From / To
    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.
    1998 University College Dublin M.Sc.

    External Collaborators

      Name Role / Description Country
    Dr Rustan Leino. Microsoft Research Research in Software Engineering and Program Verification
    Mr Keith Dooley. National University of Ireland, Maynooth PhD Supervision
    Dr. Bernhard Beckert. Karlsruhe Institute of Technology, Germany Cost Action IC0701
    Dr Vladimir Klebanov. Karlsruhe Institute of Technology, Germany Verification Competitions
    Prof Dominique Mery. INRIA, UL and LORIA Research on Modeling languages and specification e.g. Event B, Spec#
    Dr James Power. National University of Ireland, Maynooth Principles of Programming Research
    Mr Zheng Cheng. National University of Ireland, Maynooth PhD Supervision
    Dr Marieke Huisman. University of Twente, Netherlands Verification Competitions
    Mr Hao Wu. National University of Ireland, Maynooth PhD Supervision
    Prof Joseph Morris. Dublin City University PhD work - completed in 2009