Dr Rosemary Monahan

image

Contact Details

Lecturer
Office: 2.105, Callan Building, North Campus
Address: Department of Computer Science, NUI Maynooth, Maynooth Co. Kildare
image
Phone Number: +353-1-7083463/3847
Fax Number: +353-1-7083848

Qualifications

  • PhD (Dublin City University 2010)
  • MSc in Computer Science (University College Dublin, 1998 )
  • BSc in Computer Science (University College Dublin, 1995)

Research Interests

I hold BSc and MSc degrees from UCD and a PhD from DCU and have been a Computer Science Lecturer at NUIM since 1999. My research is concerned with the development of reliable software systems.

Together with my colleague Dr James Power,I have established the Principles of Programming (POP) research group at NUIM. The POP group specialise in the static and dynamic analysis of object-oriented programs and programming languages. My main research interest lies here, and more specifically in program verification. As a member of this group, I supervise PhD and MSc students and teach courses relating to Software Verification. The group currently has 4 active PhD students whose research covers topics in software specification, program verification, metamodelling and software language engineering. This research is funded via SFI, EI, Ulysses and NUIM funding. I am the Programme Director for the Erasmus Mundus MSc in Dependable Software Systems (DESEM) (funded from 2012-18), the MSc in Computer Science and the Postgraduate Diploma in Computer Science.

Current research includes collaborations on the Spec# Programming System with the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond, and on Event B with MOSEL Research Group, LORIA. My research on the automatic verification of software correctness currently focuses on “Arís: Analogical Reasoning for reuse of Implementation and Specification”. This collaboration with Dr Diarmuid O’Donoghue, applies models of analogical reasoning to the domain of reliable software development and re-use. Previous collaborations include work on verifying safety critical properties of PLC’s with TramPower UK and on the verification of SparkAda programs via intermediate representations. Through participating and judging program verification competitions, I also have an intimate knowledge of current state-of-the-art verification tools and am extremely aware of the existing tools strengths and weaknesses.

In 2010, I graduated with my PhD from the School of Computing,Dublin City University. The topic of my dissertation was "Data Refinement in Object-Oriented Verification"

In 2007, I visited Microsoft Research, Redmond labs, where I worked with the Spec# team on the automatic verification of textbook programs using Spec#. Details of this research and some sample programs in Spec# are available here.

Research for my MSc on "Deduction Based Transformational Programming", involved the study of algebraic specifications and their implementation using the method of transformational programming. The design and implementation of a tool to support this program construction was required. This work is based on the theorem prover Isabelle.

During the course of this research I spent three months at the Technical University of Munich working in Professor Broy’s school where I presented my work to members of the school. In August 1996 I obtained a scholarship to attend a Summer School in Mathematical Methods of Program Development in Marktoberdorf , Germany.

Professional Assignments

DESEM Erasmus Mundus Consortium Director 2012-2018

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


Membership of NUI Maynooth Committees

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


Member of the Program Committee/ Reviewer for

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


    • Principal Organiser for:

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


    Member of the Organising Committee for

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


    External Examiner for

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


    Other Activities

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

    Teaching and Academic Programme Directorships

    I am a full time academic in the Department of Computer Science, NUI Maynooth since October 1999. I have been lecturing in Computer Science since 1997 in University College Dublin, Griffith College Dublin and NUI Maynooth. I have also being a visiting lecturer at Universite de Lorraine in France and Zhejiang University in China. Subjects which I have lectured include Software Verification, Rigorous Software development, Type Theory, Models of Computation, Object Oriented Programming (C++, Java, C#), Object Oriented Design, Algorithms and Data Structures, Information Systems Development, Database Management Systems, Computer Graphics, Formal Methods, Program Language Semantics and Discrete Structures. This academic year (2014/2015), I am teaching:
    • CS603 - Rigorous Software Development (MSc Level)
    • CS629 - Directed Reading (MSc Level)
    • CS357 - Software Verification (3rd Year BSc Level)
    I also direct the following taught postgraduate programmes:

    Some (old) lecture slides follow. New lecture slides are available on Moodle.

    CS101 Introduction to Programming - see https://firstyears.cs.may.ie/

    CS603 Rigorous Software Process – see MSc Lab J drive

    CS613 Object-Oriented Programming and C++

    Se202 Algorithms and Data Structures

    SE119 Discrete Structures

    SE304/CS407 Formal Methods (Z Specification & Program Verification)

    SE424 Formal Methods (Program Language Semantics)

    Research Supervision

    In 2012/13 I am supervising/co-supervising:
    • Hao Wu (PhD)
    • Zheng Cheng (PhD)
    • Keith Dooley (PhD)
    • Jagadeeswaran Thangaraj(PhD)
    • Asif Saleem (MSc)
    • Peihan Li (MSc)
    • Juan Jose Mendoza(MSc)
    • Mahai Pitu (MSc)
    • Daniela Grijincu (MSc)
    • Marie Farrell(BSc)

    Supervisor of other MSc Theses and fourth year B Sc projects such as:

    Verifying Estelle Simulations of E-voting Cryptographic Protocols, Zou Weili, MSc in Computer Science, 2009, Collaborating with TELECOM & Management SudParis

    Developing a Sort Allocation Tool based on an Optimisation Model, Edward Whelehan, MSc in Computer Science, 2009, Collaborating with Intel Ireland

    Safety Critical Transport Software, Hugh Maher, B Sc (Computer Science and Software Engineering) 2009, Collaborating with LORIA and TramPower UK

    Gareth Carter’s MSc on Support tools for Object Oriented Software Development and project details are available at www.cs.nuim.ie/toolap/pd . Examples include Perfect Developer and ESC Java.

    A sample of other MSc theses and 4th year projects that I have supervised are:.

    Sample MSc theses that I have supervised

    • Implementing a web based Lab Monitoring tool to meet the need of the customer, Tarandeep Padam, MSc in Computer Science(Software Engineering) 2008
    • Improving the Software Engineering Process in Local Government, Alison Boland MSc in Software Engineering 2005
    • Machine Translation Output Evaluation, Benjamin Leduc, MSc in Software Engineering 2005(Microsoft, Ireland)
    • Object Pascal Language Recognition: A Study of ANTLR Grammar Developmemnt for Application Migration, Lee George, MSc in Software Engineering 2005
    • An Assesment of Perfect Developer, Jennifer Cunningham, Master of Computer Science 2003
    • AAT: An algorithm Animation Tool, Ciaran McKevitt, Master of Computer Science 2002
    • The Development of a Word Prediction Prototype System, Michael Tunney, Master of Computer Science 2000

     

    Sample 4th year projects that I have supervised

    • A Spec# Evaluation, Daniel Russell, BSc (Computer Science and Software Engineering) 2006
    • A Region Based Life Cycle Animation Tool, Derek Power, BSc (Computer Science and Software Engineering) 2006
    • CAVIAR (Computer Aided Visitor Information and Retrieval System), Claire Bailey, BSc (Computer Science and Software Engineering) 2005
    • A Soccer League Management System using Java and JML, Damien Fox, BSc (Computer Science and Software Engineering) 2005
    • SAADLE: Simple Algorithm Animation Design and Learning Environment, John Crawley, BSc (Computer Science and Software Engineering) 2005
    • Region Based Memory Mangement, Stephen Mooney, BSc (Computer Science and Software Engineering) 2005
    • Program Derivation, Keith Hamilton, BSc (Computer Science and Software Engineering) 2004
    • A teaching tool for Reliable Programs, Jonathan Mullaney, BSc (Computer Science and Software Engineering) 2004
    • Multimedia Applications of Educational Technologies and Tools, Brendan Pierce, BSc (Computer Science and Software Engineering) 2003
    • Developing a Bulletin Board Application, Tom Handy, BSc (Computer Science and Software Engineering) 2003
    • Football Manager Simulation, Alan Fox, BSc (Computer Science and Software Engineering) 2003

    Research Visitors Hosted

    • Erasmus Mundus Scholars 2013: Dr Kaan Kurtel, Dr Thomas Wies, Dr Petrucio Viana, Dr Sebnem Er.
    • Research Brazil Ireland: Dr Petrucio Viana, Dr Marcia Cerioli
    • Research Visit: Dr Ruzica Piskac
    • Dominique Mery, UHP, Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2009: Lectures presented to the MSc in Computer Science students on Event B and the Rodin platform and a Departmental Seminar on Case studies in Event B.
    • Dominique Mery, LORIA, Laboratoire Lorrain de Recherche en Informatique et ses Applications, Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.
    • Dominique Cansell, LORIA, Laboratoire Lorrain de Recherche en Informatique et ses Applications, Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.
    • Dominique Mery, UHP, Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2008: Lectures presented to the MSc in Computer Science students on Event B and the Rodin platform and a Departmental Seminar on Case studies in Event B.
    • Paul Gibson, Le département LOgiciels-Réseaux, Telecom & Management SudParis, Research Visit in 2008 for collaboration on teaching formal methods and presentation of research relating to the ETAPS 2008 publication "How Do I know If My Design Is Correct?"
    • K. Rustan M. Leino Microsoft Research, Redmond, Research Collaboration and Research Presentation in 2007: Program verification via an intermediate verification language
    • Anna Danko, Polish Japanese Institute of Information Technology, Warsaw, Poland, Research collaboration and presentation of research on Multi Agent Systems (May 11th and 12th, 2004)
    • Rem Collier, Department of Computer Science, University College Dublin, Research presentation on Agent Factory: A Framework for the Engineering of Agent-Oriented Applications (9th February 2004)
    • John McCormack, Hewlett Packard, Systems Research Labs, Palo Alto, Research collaboration and presentation in 2003.

    Research Funding

    • Action IC0701 of COST (2008-2012), Travel and Subsistence, European Cooperation in the field of Scientific and Technical Research, €600,R Monahan,2009
    • ULYSSES France-Ireland Exchange Programme, IRCSET , €5000,A Winstanley, R Monahan, Dept of Computer Science, NUI Maynooth D Mery, D Cansell, LORIA, Nancy,2008
    • Enterprise Ireland International Collaboration Grant 2005/49, Collaboration on Problem Based Learning with Clemson University, South Carolina, (€5400)
    • Enterprise Ireland Basic Research Grant Joint collaboration between Dublin City University and National University of Ireland, Maynooth, Ireland, TOOLAP: A Tool for Developing Object-Oriented Software, ( €139,900)
    • Enterprise Ireland Basic Research Grant Joint collaboration between Dublin City University and National University of Ireland, Maynooth, Ireland, TOOLAP: A Tool for Developing Object-Oriented Software.
    • Enterprise Ireland International Collaboration Grant 2003/112, Joint collaboration between Hewlett Packard, Systems Research Labs, Palo Alto, California and National University of Ireland, Maynooth, Ireland.
    • Enterprise Ireland International Collaboration Grant 2001/061, Joint collaboration between Clemson University, South Carolina and National University of Ireland, Maynooth, Ireland.
    • NSF Grant (US) for travel and subsistence for Proofs as Programs Summer School
    • MSc funded by Fobairt Research Grant SC/95/408

    Research Presentations

    • Deductive Verification Systems, Evaluating Software Verification Systems: Benchmarks and Competitions, Dagstuhl seminar 14171, 2014
    • Evaluating Software Verification Systems, Foundations of Computer Science Seminar Series, Dept. of Computer Science, NUIM,2014
    • An early program proof by Turing, Turing Year Seminars, Dept. of Computer Science, NUIM, 2012
    • Case Based Specifications: reusing specifications, programs and proof, AI meets Formal Software Development, Dagstuhl seminar 12271, 2012
    • Teaching Using Spec# in Europe: A Experience Report from University Teaching and Various Verification Tutorials, Microosft Faculty Summit, 2011
    • Encoding Comprehensions as First Order Expressions in Boogie, Programming Languages and Methods Group Meeting, Microsoft Research, Redmond, WA, USA, February 2008
    • Automatic Verification of C# programs, Staff Seminar Series Department of Computer Science, NUI Maynooth, Ireland , November 2007
    • Automatic Program Verification with Spec#, MOSEL Research Seminar Series, LORIA, Nancy, France, May 2007
    • Automatic verification of textbook programs that use comprehensions, Formal Techniques for Java-like Programs, Berlin, Germany , July 2007
    • Software Refinement with Perfect Developer, Software and Systems Engineering Seminar Series, NUI Maynooth, (December 2005)
    • Problem-Based Learning: A Hybrid Model, Department of Computer Science, Clemson University, (June 2005)
    • Typing in Object Oriented Languages, NUIM/DCU Seminar series, NUI Maynooth, (April 2001)
    • A DEBATE with Isabelle, Dept. of Computer Science, NUI Maynooth, (November 1999)
    • Tactics for Transformational Programming, IWFM '97, University College Dublin, (July 1997)
    • Proving Transformations in Isabelle, IFMSIG Meeting, University College Cork, (November 1996)
    • Program Construction by Transformations", Postgraduate Day, University College Dublin, (November 1996)
    • Transformational Programming, Dept. of Computer Science, University College Dublin, (September 1996)
    • Transformational Programming, Dept. of Computer Science, Technical University Munich, (July 1996)

    Industrial Collaboration

    • Microsoft Research, Redmond, WA, USA, Gratis Visitor to Microsoft Research in 2008 to prepare a tutorial on the Spec# Programming System for presentation at ETAPS 2008, to develop material for the MSc curriculum in Computer Science and to further ongoing research collaboration.
    • Trampower UK, We apply reverse-engineering techniques to an already existing tram control system, with the overall aim of verifying the correctness of its safety critical properties. We are developing tools to translate the control system from Programmable Logic to Event B.
    • Microsoft Research, Redmond, WA, USA, This research extended the Spec# programming system, increasing the categories of programs that this system could verify using the SMT solvers Simplify and Z3. In particular, we focused on extending the system so that it could be used with typical examples used in program verification
    • Escher Technologies, UK Review of the support for Refinement within the Perfect language and Perfect Developer Toolset (2003-2006)
    • Hewlett Packard, Systems Research Labs, Palo Alto, Collaboration on Programming Language Design (2003)

    Academic Collaboration

    • Henri Poincaré University, Nancy 1, France, Erasmus Teaching Exchange 2009: Lectures on the Spec# Programming System
    • Institute of Cybernetics, Tallinn University of Technology, To attend COST Action IC0701, Winter School on Verification of Object-Oriented Programs ran by a European network of researchers working on methods and tools for verification.
    • Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), France , Ulysses Visit 2008: research on translating programs for control system from Programmable Logic to Event B so that we can use formal verification tools to verify its software requirements.
    • Dublin City University, Collaboration with Prof J. Morris on Data Refinement in Object Oriented Languages.
    • MOSEL Research Group, Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Research on the formal verification and refinement of software systems using the Event-B methodology.

    Publications

    See here for details.

    Last updated April 2013