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 Data61's 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:

  • Tue, 11:00h - 13:00h AEST (online)
  • Wed, 16:00h - 18:00h AEST (online)
  • Lectures are running weeks 1-10, delivery is online in T3 2020
  • Please see here and here for UNSW information on Covid-19

Lectures

Slides and Isabelle files will be made available online as the lectures progress.

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, untyped lambda calculus

slides [pdf], slides with animations [pdf], intro demo [thy], lambda calculus demo [thy]

Week 1 (B): typed lambda calculus

slides [pdf], slides with animations [pdf], demo [thy]

Week 2 (A): HOL, natural deduction for propositional logic

slides [pdf], slides with animations [pdf], demo [thy] demo solution [thy]

Week 2 (B): HOL, quantifiers, automation, Isar (part 1)

slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy], Isar demo [thy]

Week 3 (A): more automation, defining HOL from scratch

slides [pdf], slides with animations [pdf], HOL demo [thy] automation demo [thy]

Week 3 (B): term rewriting, confluence, termination

slides [pdf], slides with animations [pdf], introductory demo [thy] simp demo [thy]

Week 4 (A): conditional term rewriting, congruence rules, more confluence

slides [pdf], slides with animations [pdf], demo [thy]

Week 4 (B): sets, type definitions, inductive predicates

slides [pdf], slides with animations [pdf], demo [thy], demo solutions [thy]

Week 5 (A): inductive predicates, rule induction formally

slides [pdf], slides with animations [pdf], demo [thy], solution [thy]

Week 5 (B): datatypes, datatype induction, primitive recursion

slides [pdf], slides with animations [pdf], demo [thy]

Week 7 (A): rule induction tutorial

demo [thy] (as developed in the lecture + bonus content)

Week 7 (B): general recursive functions

slides [pdf], slides with animations [pdf], demo [thy]

Assignment 1

  • Assignment [pdf]
  • Isabelle template [thy]
  • LaTeX style for type trees (optional) [sty]

You may collect your marked assignment. Run (on a CSE machine):

~cs4161/bin/classrun -collect a1

or use the web interface.

Model assignment solution: [thy]

Assignment 2

Assignment submission

submit using give:

give cs4161 a2 a2.thy

You can also use the web interface.

Assignment 3

To be announced

Exam

The exam will be a 24h take-home exam. Details to be confirmed later.

Contact

Forum

We are using Piazza for class discussions. Please post questions about lecture material or the assignments and so forth.

Lecturers

Consults by appointment.