This course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade interactive theorem provers (Isabelle/HOL), 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.
Note: This course is based on the course Advanced Topics in Software Verification offered by UNSW.
Learning Outcomes
- write definitions in the theorem prover Isabelle/HOL formalise software verification problems
- prove theorems in an interactive proof assistant effectively use proof automation and automatic counter-example finding
- formally verify functional programs
- formally verify imperative programs, including small C programs
Workload
Combination of Class hours and self study to total 130-140 hours.
Requisite and Incompatibility
12 unit 3000 level COMP courses and COMP2620/6262 Logic. COMP 3610/6361 Principles of Programming Languages not mandatory, but benefitial. You will need to contact the School of Computing to request a permission code to enrol in this course.
If you’re stuck, then you can reach out for help anytime—the course help page or course forum is a good place to start.