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:

  • Wed, 16:00h - 18:00h AEDT (online)
  • Fri, 15:00h - 17:00h AEDT (online)
  • Lectures are running weeks 1-10, delivery is online in T3 2023. The Zoom will be found on Moodle (but not yet).

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], "whiteboard" [txt] [thy]

Week 1 (B): typed lambda calculus

slides [pdf], slides with animations [pdf] (which we did not get to in W1), "whiteboard" [txt], lambda calculus demo [thy] demo [thy]

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

slides [pdf], slides with animations [pdf], demo [thy], demo solution [thy], "whiteboard" [txt]

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

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

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

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

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

Week 7 (A): primrec and rule induction tutorial (regular expressions)

demo (as developed in the lecture) [thy]

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 (part 1) [thy] Isar demo (part 2) [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: [s2.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]

Contact

Forum

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

Lecturers

Consults by appointment.