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 from Proofcraft and UNSW. 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:

  • Mon, 10:00h - 12:00h AEDT (online)
  • Thu, 09:00h - 11:00h AEDT (online)
  • Lectures are running weeks 1-10, delivery is online in T3 2021
  • 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.

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] exercise template [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] solution [thy]

Week 7 (A): primrec and rule induction tutorial

demo [thy] (as developed in the lecture)

Week 7 (B): general recursive functions

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

Week 8 (A): automatic proof and disproof, Isar (part 2)

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

Week 8 (B): Semantics and Hoare logic

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

Week 9 (A): Weakest precondition, verification condition

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

Week 9 (B): Shallow Embedding, State Monads

  • slides [pdf]
  • slides with animations [pdf]
  • records demo [thy]
  • monad demo (Monads) [thy]
  • monad demo (Monads solution) [thy]
  • monad demo (GCD) [thy]
  • monad demo (GCD solution) [thy]
  • monad demo (While) [thy]

Week 10 (A): C verification, AutoCorres

slides [pdf], slides with animations [pdf], demo [thy], C file [c],
C-Parser and AutoCorres [tar.gz]

Week 10 (B): exam preparation

slides [pdf], slides with animations [pdf], 2014 exam papers: exam [pdf], C file [c], Isabelle template [thy].
2014 exam solution: [pdf, thy].
invariant practice demo [thy] and solutions [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

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

~cs4161/bin/classrun -collect a2

or use the web interface.

Model assignment solution: [thy]

Assignment 3

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

~cs4161/bin/classrun -collect a3

or use the web interface.

Model assignment solution: [thy]

Exam

The exam will be a 24h take-home exam. It will start Mon, 29 Nov 2021, 8am AEDT (Sydney time), and end Tue, 3 Dec 2021, 7:59am AEDT (Sydney time).

Exam material:

You should use Isabelle 2021 and AutoCorres-1.8 for the exam (same as for assignment 3).

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

~cs4161/bin/classrun -collect exam

or use the web interface.

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.