Students

COMP4000 – Formal Methods

2025 – Session 1, In person-scheduled-weekday, North Ryde

General Information

Download as PDF
Unit convenor and teaching staff Unit convenor and teaching staff Convenor, lecturer
Annabelle McIver
Lecturer, Tutor
Chris Chen
Credit points Credit points
10
Prerequisites Prerequisites
COMP3000 and COMP3010
Corequisites Corequisites
Co-badged status Co-badged status
Unit description Unit description

This unit provides a study of rigorous mathematical methods to model and analyse software systems. Topics covered include: formal specification, validation, verification techniques, automata based modelling, model-checking techniques, and program correctness.

Learning in this unit enhances student understanding of global challenges identified by the United Nations Sustainable Development Goals (UNSDGs) Quality Education; Industry, Innovation and Infrastructure; Peace, Justice and Strong Institutions

Important Academic Dates

Information about important academic dates including deadlines for withdrawing from units are available at https://www.mq.edu.au/study/calendar-of-dates

Learning Outcomes

On successful completion of this unit, you will be able to:

  • ULO1: Use mathematical models to describe software systems.
  • ULO2: Write formal specifications of software systems.
  • ULO3: Use state-of-the-art formal methods and tools to specify and analyse software systems.
  • ULO4: Apply formal methods in software engineering design.

General Assessment Information

Release Dates for Assessments

o Assignment: To be released no later than 24th March.

o Summative integrative task (project): To be released no later than 19th May.

Late Assessment Submission Penalty 

Unless a Special Consideration request has been submitted and approved, a 5% penalty (of the total possible mark of the task) will be applied for each day a written report or presentation assessment is not submitted, up until the 7th day (including weekends). After the 7th day, a grade of ‘0’ will be awarded even if the assessment is submitted. The submission time for all uploaded assessments is 11:55 pm. A 1-hour grace period will be provided to students who experience a technical concern. For any late submission of time-sensitive tasks, such as scheduled tests/exams, performance assessments/presentations, and/or scheduled practical assessments/labs, please apply for Special ConsiderationFor example, if the assignment is worth 8 marks (of the entire unit) and your submissionis late by 19 hours (or 23 hours 59 minutes 59 seconds), 0.4 marks (5% of 8 marks) will be deducted. If your submission is late by 24 hours (or 47 hours 59 minutes 59 seconds), 0.8 marks (10% of 8 marks) will be deducted, and so on.

Assessments where Late Submissions will be accepted 

In this unit, late submissions will accepted as follows:

Assignment: YES, Standard late penalty applies

Project: YES, Standard late penalty applies

Homework quizzes: NO, Unless special consideration is granted

Special Consideration

 The Special Consideration Policy aims to support students who have been impacted by short-term circumstances or events that are serious, unavoidable and significantly disruptive, and which may affect their performance in assessment. If you experience circumstances or events that affect your ability to complete the assessments in this unit on time, please inform the convenor and submit a Special Consideration request through ask.mq.edu.au.

Requirements to Pass this Unit

To pass this unit you must achieve a total mark equal to or greater than 50%

Assessment Tasks

Name Weighting Hurdle Due
Summative integrative task 35% No Sunday 8 June, 11:55pm
Assignment 30% No Sunday 13 March, 11:55pm
Weekly homeworks 35% No Throughout the semester

Summative integrative task

Assessment Type 1: Project
Indicative Time on Task 2: 24 hours
Due: Sunday 8 June, 11:55pm
Weighting: 35%

 

The project requires the application of the techniques learned throughout the unit to demonstrate facility at software verification, validation and/or modelling.

 


On successful completion you will be able to:
  • Use mathematical models to describe software systems.
  • Write formal specifications of software systems.
  • Use state-of-the-art formal methods and tools to specify and analyse software systems.
  • Apply formal methods in software engineering design.

Assignment

Assessment Type 1: Programming Task
Indicative Time on Task 2: 24 hours
Due: Sunday 13 March, 11:55pm
Weighting: 30%

 

Development of, and from, a formal specification

 


On successful completion you will be able to:
  • Write formal specifications of software systems.
  • Apply formal methods in software engineering design.

Weekly homeworks

Assessment Type 1: Quiz/Test
Indicative Time on Task 2: 24 hours
Due: Throughout the semester
Weighting: 35%

 

Formal verification and modelling problems

 


On successful completion you will be able to:
  • Use mathematical models to describe software systems.
  • Use state-of-the-art formal methods and tools to specify and analyse software systems.

1 If you need help with your assignment, please contact:

  • the academic teaching staff in your unit for guidance in understanding or completing this type of assessment
  • the Writing Centre for academic skills support.

2 Indicative time-on-task is an estimate of the time required for completion of the assessment task and is subject to individual variation

Delivery and Resources

Technologies Required

COMP4000 is a BYOD (Bring Your Own Device) unit. You will be expected to bring your own laptop computer (Windows, Mac, or Linux) to the workshop, install and configure the required software, and incorporate secure practices into your daily work (and play!) routines. The laptop must be capable of running the Dafny verification tool; details are available from the Dafny installation page. It has been tested on a number of standard set ups.

Other software that might be useful include Java SE JDK, and Python.  

Learning Management System iLearn : This will be used primarily to enable email broadcasts and give access to Assessment marks. The lecture audio will be recorded, and will be available via iLearn. Workshops will not be recorded.

Methods of Communication

General information about assessments and other learning activities will be through broadcasts over the iLearn announcement forum.

If students need to contact the teaching staff, please speak to them during the workshops or contact them by email, (addresses available on the unit's iLearn pages). If the topic is about general questions regarding the assessments or other unit activities, please post a question on the relevant iLearn forum.

Classes

Week 1 classes: There will be a lecture in Week 1 but no workshops.

Each subsequent week there are 2 hours of lectures and a two-hour workshop. For details of days, times and rooms consult the timetables webpage.

You should have selected one two-hour workshops session at enrolment. You should go to the session you are enrolled in.

Please note that you are expected to be present at most of the workshops because that is your opportunity to seek clarification of any parts of the course and exercises you do not understand. Note that the quizzes and assignments will be strongly based on the exercises you will complete during the workshops. You are therefore strongly advised to participate in the class exercises, and to seek clarification when you are unable to complete a question. 

Unit Pages

The unit will make use of discussions hosted within iLearn. Please post questions there, they will be monitored by the staff on the unit.

Teaching and Learning Strategy

COMP4000 is taught via lectures and workshops. Lectures are used to introduce new theoretical material and methods, to give examples of the use these techniques and put them in a wider context. Workshops give you the opportunity to interact with your peers. You will be given problems to solve each week prior to each session; preparing solutions is important because it will allow you to discuss the problems effectively with your tutor thereby making the most of this activity. The aim of the workshops is to help you to develop problem-solving skills and teamwork, and you will be expected to work on problems in class.

There will be an opportunity to explore more deeply aspects of the course material which has not been covered in lectures or classes. These will sometimes be student-led, and in various forms including Q&A with the lecturer or short videos. Topics will for example include questions not covered in workshops, or hints and tips for assignments. More information for the timing of these sessions will be available on iLearn.

Lecture notes will be made available each week but these notes are intended as an outline of the lecture only and are not a substitute for your own notes or the textbook.

Standards and Grading

 The final mark for the unit will be calculated by combining the marks for all assessment tasks according to the percentage weightings shown in the assessment summary.

Extension requests

Please note if you cannot submit on time because of illness or other circumstances, please contact the lecturer before the due date. If you experience a disruption to studies, you should notify the university.  Please note that this is a centralised process, and resolution can take some time.  This may mean, for example, that you are notified that your disruption request has been approved only after any reasonable length extension for an assignment could be granted: for instance, the assignment might have already been handed back.  With respect to assignments, you should therefore also notify the lecturer responsible for the assignment, and submit a solution to the assignment via iLearn, at the same time as you lodge your official disruption notification.  Failure to do so means that an extension may not be possible, leaving only some other remedy listed under the disruption to study outcomes schedule (e.g. partake in assessment task next available session).

Unit Schedule

Weeks 1–3:  Introduction to formal specification and verification

Weeks 2–6:  Developing programs that satisfy specifications

Weeks 7--9:  Formal modelling using the Dafny programming language

Weeks 8–12: Formal methods for concurrency

Week 13: Review

Policies and Procedures

Macquarie University policies and procedures are accessible from Policy Central (https://policies.mq.edu.au). Students should be aware of the following policies in particular with regard to Learning and Teaching:

Students seeking more policy resources can visit Student Policies (https://students.mq.edu.au/support/study/policies). It is your one-stop-shop for the key policies you need to know about throughout your undergraduate student journey.

To find other policies relating to Teaching and Learning, visit Policy Central (https://policies.mq.edu.au) and use the search tool.

Student Code of Conduct

Macquarie University students have a responsibility to be familiar with the Student Code of Conduct: https://students.mq.edu.au/admin/other-resources/student-conduct

Results

Results published on platform other than eStudent, (eg. iLearn, Coursera etc.) or released directly by your Unit Convenor, are not confirmed as they are subject to final approval by the University. Once approved, final results will be sent to your student email address and will be made available in eStudent. For more information visit connect.mq.edu.au or if you are a Global MBA student contact globalmba.support@mq.edu.au

Academic Integrity

At Macquarie, we believe academic integrity – honesty, respect, trust, responsibility, fairness and courage – is at the core of learning, teaching and research. We recognise that meeting the expectations required to complete your assessments can be challenging. So, we offer you a range of resources and services to help you reach your potential, including free online writing and maths support, academic skills development and wellbeing consultations.

Student Support

Macquarie University provides a range of support services for students. For details, visit http://students.mq.edu.au/support/

The Writing Centre

The Writing Centre provides resources to develop your English language proficiency, academic writing, and communication skills.

The Library provides online and face to face support to help you find and use relevant information resources. 

Student Services and Support

Macquarie University offers a range of Student Support Services including:

Student Enquiries

Got a question? Ask us via the Service Connect Portal, or contact Service Connect.

IT Help

For help with University computer systems and technology, visit http://www.mq.edu.au/about_us/offices_and_units/information_technology/help/

When using the University's IT, you must adhere to the Acceptable Use of IT Resources Policy. The policy applies to all who connect to the MQ network including students.


Unit information based on version 2025.03 of the Handbook