Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 25 additions & 0 deletions Research/courses.html
Original file line number Diff line number Diff line change
Expand Up @@ -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="
<p>
<strong>Software Verification using Proof Assistants</strong>
</p>
<p>
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, which is used in the verification of seL4.
</p>"
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"
%}
Loading