COMP4161: Advanced Topics in Software Verification

Prerequisites:

The course covers a lot of theory regarding automated theorem provers and the foundations such as lambda calculus, but the assessments are generally quite practical, and it has a large focus on learning how to use Isabelle itself. A pretty interesting course overall, especially towards the end where the focus shifts to verifying C code using Isabelle. A lot of the theory involves some familiarity with mathematical proofs and notation. The proofs in Isabelle are generally made easier if you can reason logically to guide the proof as well, though you can sometimes just bruteforce it.
Content-wise, the course covers untyped and typed lambda calculus and higher-order logic before diving into the concepts the internals of Isabelle are built upon; rule induction, inductive datatypes, confluence, and how Isabelle handles these internally. The course ends teaching how AutoCorres translates C code to a meta language that can be reasoned about using Isabelle to prove properties of programs with Hoare logic.

2x 2hr Lectures

3.5/5

Yes, all recorded.

Prof. Gerwin Klein, Dr. Johannes Pohjola, Dr. Christine Rizkallah, and Dr. Miki Tanaka

Lecture slides, assignment solutions, and lecture demos all available online.

4/5

2020 T3

95 HD