From 0944def860e3e96453f66c5326999b06f12d0e5f Mon Sep 17 00:00:00 2001 From: "b@brck.nl" Date: Wed, 4 Nov 2026 12:44:11 +1100 Subject: [PATCH 1/2] update courses - add anu update courses - add anu Signed-off-by: b@brck.nl --- Research/courses.html | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/Research/courses.html b/Research/courses.html index 3ce32cab2..cdcde4f13 100644 --- a/Research/courses.html +++ b/Research/courses.html @@ -97,3 +97,28 @@ alt="Picture of the Concrete Semantics book" img_class="p-white" %} +{% include feature.html + right=true + up=true + h2="Advanced Topics in Formal Methods and Programming Languages (COMP4011/8011)" + text=" +

+ Software Verification using Proof Assistants +

+

+ 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. + The course will provide hands-on experience with the proof assistant + Isabelle/HOL. +

" + link="https://programsandcourses.anu.edu.au/2026/course/COMP4011/Second%20Semester/9011" + button=button + img="/Foundation/Membership/LOGOS/anu.svg" + alt="ANU School of Computing logo" + img_class="p-white" +%} \ No newline at end of file From 04b69615dcf80ab81374790725a6ff0b47740c79 Mon Sep 17 00:00:00 2001 From: bbrcknl <32238793+bbrcknl@users.noreply.github.com> Date: Fri, 13 Nov 2026 07:05:18 +1100 Subject: [PATCH 2/2] Update Research/courses.html Co-authored-by: June Andronick Signed-off-by: bbrcknl <32238793+bbrcknl@users.noreply.github.com> --- Research/courses.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Research/courses.html b/Research/courses.html index cdcde4f13..d48f8ea3f 100644 --- a/Research/courses.html +++ b/Research/courses.html @@ -114,7 +114,7 @@ order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, and proofs about programs. The course will provide hands-on experience with the proof assistant - Isabelle/HOL. + Isabelle/HOL, which is used in the verification of seL4.

" link="https://programsandcourses.anu.edu.au/2026/course/COMP4011/Second%20Semester/9011" button=button