Assignments
There will be three marked assignments in the course. The schedule and marking formula are described in the lecture slides and in the informal course outline.
COMP4161 
Advanced Topics in Software Verification
This UNSW course is about
mechanical proof assistants, how they work, and what they can be used
for. It is taught by members of the
Trustworthy Systems
group.
The course presents specification and proof techniques used in
industrial grade interactive theorem provers, teaches the theoretical background
to the techniques involved, and shows how to use a theorem prover to
conduct formal proofs in practice.
Topics include higher order logic, natural deduction, lambda calculus,
term rewriting, data types and recursive functions, induction
principles, and proofs about
programs. See the course outline for a full
content overview and prerequisites.
The course will provide hands-on experience with the proof assistant Isabelle/HOL.
Session times for 2026 T3:
- Tue, 14:00h - 16:00h AEST @ E8 Science and Engineering Building G05 (K-E8-G05)
- Thu, 16:00h - 18:00h AEST @ E8 Science and Engineering Building G05 (K-E8-G05)
- Lectures are running weeks 1-5 and 7-10, delivery is hybrid in T3 2026. The Zoom link will be posted on the forum.
- Lecture recordings can be found on Echo360 via the course moodle page.
Lectures
Slides and Isabelle files will be made available online as the lectures progress.
Lecture recordings can be found on Echo360 via the course moodle page.
Isabelle hints
Setting up Isabelle, basic rules and cheat sheet.
Textbook
Textbook, further reading, and links the tools used in the lecture.
Slides
Will become available here as course progresses.
Week 1 (A): intro
slides [pdf], slides with animations [pdf], intro demo [thy], lambda calculus demo [thy], more demo to come
Second lecture: typed lambda calculus
slides [pdf], slides with animations [pdf], demo [thy]. Lecture will continue into week 2.
Seven Bridges Exercise
Week 2 (A): HOL, natural deduction for propositional logic
Assignment 1
- Assignment pdf and Isabelle template are available from the course moodle page.
Assignment submission
submit using give:
give cs4161 a1 a1.thy
You can also use the web interface.
Contact
Forum
We are using this Discourse forum for class discussions. Please post questions about lecture material, the assignments and so forth on the forum.
Lecturers
Consults by appointment.