This course offers students a unique opportunity for the advanced study of a special thematic area within the discipline of Theoretical Computer Science. The topics will vary from year to year in response to emerging theoretical and practical issues in the discipline, as well as the research interests and expertise of academics and sessional staff. They will be drawn from the broad areas of formal methods and programming languages, and could include (but not limited to) the following topics: computational logic, category theory, concurrency theory, type theory, semantics of programming languages, computer-assisted theorem proving, model checking, formal methods for security, and formal verification of hardware and software systems.

Learning Outcomes

Upon successful completion, students will have the knowledge and skills to:

1.  Demonstrate a broad knowledge in the advanced topic and its role and applications in modern computing systems
2. Critically evaluate the scientific literature related to the advanced topic and/or applications of the advanced topic in modern computing systems
3. Plan and execute project work and/or a piece of research and scholarship in the advanced topic

Research-Led Teaching

This course is delivered by an active researcher in formal methods and software verification. Examples and case studies are drawn from contemporary verification research, such as the seL4 verified microkernel, and the later modules connect directly to current research questions in the field.

Required Resources

• A laptop able to run Isabelle/HOL (or use of the provided lab machines).
• Isabelle/HOL (current release) -- free and open-source; installation instructions are on the course Canvas site.
• Textbook: T. Nipkow and G. Klein, Concrete Semantics with Isabelle/HOL, Springer, 2014 -- freely available at http://concrete-semantics.org.

Recommended Resources

• T. Nipkow, Programming and Proving in Isabelle/HOL (the prog-prove tutorial shipped with Isabelle).
• T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic (LNCS 2283).
• The Isabelle documentation and reference manuals (bundled with the Isabelle distribution).

Staff Feedback

Students will be given feedback in the following forms in this course:

• written comments,
• verbal comments,
• feedback to whole class, groups, individuals, focus group etc.

Student Feedback

ANU is committed to the demonstration of educational excellence and regularly seeks feedback from students. Students are encouraged to offer feedback directly to their Course Convener or through their College and Course representatives (if applicable). Feedback can also be provided to Course Conveners and teachers via the Student Experience of Learning & Teaching (SELT) feedback program. SELT surveys are confidential and also provide the Colleges and ANU Executive with opportunities to recognise excellent teaching, and opportunities for improvement.

Other Information

Generative AI

This course introduces both fundamental and advanced concepts, some of which can potentially be addressed by certain generative AI tools (e.g., ChatGPT). Hence, the use of any generative AI tools is permitted, provided proper acknowledgment and citation are given, unless stated otherwise in the details of assessment tasks.

Class Schedule

Week/Session	Summary of Activities	Assessment
1	Introduction, Course Overview
2	Lambda Calculus
3	Isabelle Fundamentals
4	Structured Proofs I
5	HOL & Rewriting
6	Sets, Datatypes, Induction
7	Recursion
8	Structured Proofs II
9	Automation
10	Hoare Logic
11	Advanced Topics in Software Verification

Tutorial Registration

There are no tutorials in this course; only drop-in sessions (voluntarily)

Assessment Summary

Assessment task	Value	Due Date	Return of assessment	Learning Outcomes
Quizzes	5 %	30/10/2026	*	1
Test 1 (Self-Scheduled)	10 %	28/08/2026	04/09/2026	1
Homework 1	15 %	30/10/2026	*	1,3
Reflection on Homework 1	10 %	06/11/2026	*	1,2
Test 2 (Self-Scheduled)	15 %	30/10/2026	*	1,2
Homework 2	15 %	30/10/2026	*	1,3
Reflection on Homework 2	10 %	06/11/2026	*	1,2,3
Homework 3	10 %	30/10/2026	*	1,3
Presentation on Homework 3	10 %	06/11/2026	*	1,2,3

* If the Due Date and Return of Assessment date are blank, see the Assessment Tab for specific Assessment Task details

Policies

ANU has educational policies, procedures and guidelines , which are designed to ensure that staff and students are aware of the University’s academic standards, and implement them. Students are expected to have read the Academic Integrity Rule before the commencement of their course. Other key policies and guidelines include:

• Academic Integrity Policy and Procedure
• Student Assessment (Coursework) Policy and Procedure
• Extenuating Circumstances Application
• Student Surveys and Evaluations
• Deferred Examinations
• Student Complaint Resolution Policy and Procedure
• Code of practice for teaching and learning

Assessment Requirements

The ANU is using Turnitin to enhance student citation and referencing techniques, and to assess assignment submissions as a component of the University's approach to managing Academic Integrity. For additional information regarding Turnitin please visit the Academic Skills website. In rare cases where online submission using Turnitin software is not technically possible; or where not using Turnitin software has been justified by the Course Convener and approved by the Associate Dean (Education) on the basis of the teaching model being employed; students shall submit assessment online via ‘Canvas’ outside of Turnitin, or failing that in hard copy, or through a combination of submission methods as approved by the Associate Dean (Education). The submission method is detailed below.

Moderation of Assessment

Marks that are allocated during Semester are to be considered provisional until formalised by the College examiners meeting at the end of each Semester. If appropriate, some moderation of marks might be applied prior to final results being released.

Assessment Task 1

Quizzes

Quizzes at the end of each (Canvas) module to monitor progress and provide feedback regarding basic understanding of the material. 0.5% for each completed quiz for Modules 2-11. 

Recommended Due Date: 1 quiz per week, starting in Week 2.

Latest Due Date: 30/10, 11:59pm (End of Week 12)

Assessment Task 2

Test 1 (Self-Scheduled)

Self-scheduled assessment (in-person, on-campus). It will involve students proving simple properties in Isabelle/HOL. There will be no access to generative AI tools. A student scoring below 50% on an attempt may reattempt; a passing attempt is final. Students can attempt this assessment up to 3 times; the maximum awarded mark decreases each attempt (1st: 10%, 2nd: 8%, 3rd: 5%). Only attempts prior to the due date count.

This is a hurdle assessment: to pass the course, a student must achieve at least 50% in Test 1 (best counting attempt).

First Due Date: First attempt must be taken before 28/08 (otherwise the first attempt is marked as failed); subsequent attempts are permitted until the latest due date.

Recommended Due Date: 04/09, 11:59pm (End of Week 6)

(Latest) Due date: 30/10, 11:59pm (End of Week 12)

Assessment Task 3

Homework 1

To support on-going learning of the course content, three individual take-home assignments (homework) are given, distributed over the entire semester. The homework will be marked based on the submitted files. For Homework 1 the use of generative AI is discouraged, but not forbidden. This recommendation is to encourage students to build their basic understanding of interactive theorem provers.

Recommended Due Date: 09/10 (End of Week 9)

(Latest) Due date: 30/10, 11:59pm (End of Week 12)

Assessment Task 4

Reflection on Homework 1

A short oral discussion between student and lecturer (or delegate) around Homework 1 during a drop-in session. Students must reflect on challenges faced while working on Homework 1 as well as lessons learned. Details of the submission may be discussed as well.

Recommended Due Date: drop-in session the week after submission of Homework 1.

(Latest) Due date: 06/11, 11:59pm (End of Week 13)

Assessment Task 5

Test 2 (Self-Scheduled)

Self-scheduled assessment (in-person, on-campus). It will involve students proving simple properties in Isabelle/HOL. There will be no access to generative AI tools. A student scoring below 50% on an attempt may reattempt; a passing attempt is final. Students can attempt this assessment up to 3 times; the maximum awarded mark decreases each attempt (1st: 15%, 2nd: 12%, 3rd: 7%). Only attempts prior to the due date count.

This is a hurdle assessment: to pass the course, a student must achieve at least 50% in Test 2 (best counting attempt).

Recommended Due Date: The week after the Hoare Logic module has been completed.

Latest due date: 30/10, 11:59pm (End of Week 12)

Assessment Task 6

Homework 2

To support on-going learning of the course content, three individual take-home assignments (homework) are given, distributed over the entire semester. The homework will be marked based on the submitted files. For Homework 2 the use of generative AI is allowed, but requires proper citation (see ANU policies and regulation).

Recommended Due Date: 23/10 (End of Week 11)

(Latest) Due date: 30/10, 11:59pm (End of Week 12)

Assessment Task 7

Reflection on Homework 2

A short oral discussion between student and lecturer (or delegate) around Homework 2 during a drop-in session. Students must reflect on challenges faced while working on Homework 2 as well as lessons learned. Details of the submission may be discussed as well.

Recommended Due Date: drop-in session the week after submission of Homework 2.

(Latest) Due date: 06/11, 11:59pm (End of Week 13)

Assessment Task 8

Homework 3

The core assessment (Tasks 1-7) sums to 80%. Homework 3 and its presentation (Task 9) together account for 20% and are an optional, open-ended extension for students aiming at the top of the grade range. They are not required to pass or to do well in the course, but attempting them is the expected route to the upper High Distinction band. Homework 3 is an open-ended task based on a chosen topic from Module 11 (Advanced Topics in Software Verification) and will be marked based on the submitted files. For Homework 3 the use of generative AI is allowed, but requires proper citation (see ANU policies and regulation).

Recommended Due Date: 30/10 (End of Week 12)

(Latest) Due date: 30/10, 11:59pm (End of Week 12)

Assessment Task 9

Presentation on Homework 3

A short oral presentation of the ideas, achievements, and challenges of Homework 3. All enrolled students will be invited to the presentation.

Due Date: Expected Wednesday 04/11 (to be confirmed)

Academic Integrity

Academic integrity is a core part of the ANU culture as a community of scholars. The University’s students are an integral part of that community. The academic integrity principle commits all students to engage in academic work in ways that are consistent with, and actively support, academic integrity, and to uphold this commitment by behaving honestly, responsibly and ethically, and with respect and fairness, in scholarly practice.

The University expects all staff and students to be familiar with the academic integrity principle, the Academic Integrity Rule 2021, the Policy: Student Academic Integrity and Procedure: Student Academic Integrity, and to uphold high standards of academic integrity to ensure the quality and value of our qualifications.

The Academic Integrity Rule 2021 is a legal document that the University uses to promote academic integrity, and manage breaches of the academic integrity principle. The Policy and Procedure support the Rule by outlining overarching principles, responsibilities and processes. The Academic Integrity Rule 2021 commences on 1 December 2021 and applies to courses commencing on or after that date, as well as to research conduct occurring on or after that date. Prior to this, the Academic Misconduct Rule 2015 applies.

 

The University commits to assisting all students to understand how to engage in academic work in ways that are consistent with, and actively support academic integrity. All coursework students must complete the online Academic Integrity Module (Epigeum), and Higher Degree Research (HDR) students are required to complete research integrity training. The Academic Integrity website provides information about services available to assist students with their assignments, examinations and other learning activities, as well as understanding and upholding academic integrity.

Online Submission

You will be required to electronically sign a declaration as part of the submission of your assignment. Please keep a copy of the assignment for your records. Unless an exemption has been approved by the Associate Dean (Education) submission must be through Turnitin.

Hardcopy Submission

n/a

Late Submission

Late submission not permitted. If submission of assessment tasks without an extension after the due date is not permitted, a mark of 0 will be awarded.

Referencing Requirements

The Academic Skills website has information to assist you with your writing and assessments. The website includes information about Academic Integrity including referencing requirements for different disciplines. There is also information on Plagiarism and different ways to use source material. Any use of artificial intelligence must be properly referenced. Failure to properly cite use of Generative AI will be considered a breach of academic integrity.

Extensions and Penalties

Extensions and late submission of assessment pieces are covered by the Student Assessment (Coursework) Policy and Procedure. Extensions may be granted for assessment pieces that are not examinations or take-home examinations. If you need an extension, you must request an extension in writing on or before the due date. If you have documented and appropriate medical evidence that demonstrates you were not able to request an extension on or before the due date, you may be able to request it after the due date.

Resubmission of Assignments

See description of assessment tasks.

Privacy Notice

The ANU has made a number of third party, online, databases available for students to use. Use of each online database is conditional on student end users first agreeing to the database licensor’s terms of service and/or privacy policy. Students should read these carefully. In some cases student end users will be required to register an account with the database licensor and submit personal information, including their: first name; last name; ANU email address; and other information.
In cases where student end users are asked to submit ‘content’ to a database, such as an assignment or short answers, the database licensor may only use the student’s ‘content’ in accordance with the terms of service – including any (copyright) licence the student grants to the database licensor. Any personal information or content a student submits may be stored by the licensor, potentially offshore, and will be used to process the database service in accordance with the licensors terms of service and/or privacy policy.
If any student chooses not to agree to the database licensor’s terms of service or privacy policy, the student will not be able to access and use the database. In these circumstances students should contact their lecturer to enquire about alternative arrangements that are available.

Distribution of grades policy

Academic Quality Assurance Committee monitors the performance of students, including attrition, further study and employment rates and grade distribution, and College reports on quality assurance processes for assessment activities, including alignment with national and international disciplinary and interdisciplinary standards, as well as qualification type learning outcomes.

Since first semester 1994, ANU uses a grading scale for all courses. This grading scale is used by all academic areas of the University.

Support for students

The University offers students support through several different services. You may contact the services listed below directly or seek advice from your Course Convener, Student Administrators, or your College and Course representatives (if applicable).

• ANU Health, safety & wellbeing for medical services, counselling, mental health and spiritual support
• ANU Accessibility for students with a disability or ongoing or chronic illness
• ANU Dean of Students for confidential, impartial advice and help to resolve problems between students and the academic or administrative areas of the University
• ANU Academic Skills supports you make your own decisions about how you learn and manage your workload.
• ANU Counselling promotes, supports and enhances mental health and wellbeing within the University student community.
• ANUSA supports and represents all ANU students