We strongly encourage all students to participate actively in all learning activities. Regular engagement is crucial for your success in this unit, as these activities provide opportunities to deepen your understanding of the material, collaborate with peers, and receive valuable feedback from instructors to assist in completing the unit assessments. Your active participation enhances your learning experience and contributes to a vibrant and dynamic learning environment for everyone.

Release Dates for Assessments

We strongly encourage all students to participate actively in all learning activities

• Assignment: To be released no later than 23rd March.
• Summative integrative task (portfolio): To be released no later than 18th May.

Late Submission Policy

• 5% penalty per day: If you submit your assessment late, 5% of the total possible marks will be deducted for each day (including weekends), up to 7 days.

  • Example 1 (out of 100): If you score 85/100 but submit 20 hours late, you will lose 5 marks and receive 80/100.

  • Example 2 (out of 30): If you score 27/30 but submit 1 day late, you will lose 1.5 marks and receive 25.5/30.

• After 7 days: Submissions more than 7 days late will receive a mark of 0.

• Extensions:

  • Automatic short extension: Some assessments are eligible for automatic short extension. You can only apply for an automatic short extension before the due date.

  • Special Consideration: If you need more time due to serious issues and for any assessments that are not eligible for Short Extension, you must apply for Special Consideration.

Need help? Review the Special Consideration page HERE

Requirements to Pass this Unit

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

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).

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