seL4-related Courses

The course, offered at UNSW Sydney, Australia, provides students with a deep understanding of modern operating system technology, implementation techniques and research issues. It develops general “systems skills”, the ability to design, implement and understand a complex software system. It specifically provides a thorough understanding of low-level system software and its interaction with hardware, the trade-offs that determine system performance, techniques to assess performance correctly, and the impact of system design on security. The course is based on seL4 and students build an seL4-based operating system. Free videos of the lectures are available online.

This course, offered at UNSW Sydney, Australia, 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, 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 provides hands-on experience with the proof assistant Isabelle/HOL, which is used in the verification of seL4. The slides are available for free from the course website.

This book introduces semantics of programming languages through the medium of the proof assistant Isabelle/HOL, which is used in the verification of seL4. The book consists of two parts: a self-contained introduction to the proof assistant Isabelle, and an introduction to semantics and its applications. It contains 115 exercises that provide hands-on experience with Isabelle. Extensively classroom-tested slides are also available.