Dr Rosemary Monahan

Biography
Research Interests
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
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 |