Coursework

We deliver courses at UNSW and ANU which are aimed at supporting our educational agenda.

The courses we provide or contribute to are in the systems and formal methods areas, and are all aimed at providing strong insights and accompanied by significant practical components. Some of the courses can be taken both at post graduate and undergraduate level.

Operating Systems

Normally taken in first term of third year. The course is loosely aligned with Andy Tannenbaum's book Modern Operating Systems. Tannenbaum's book acts as a reference for classical OS theory topics, but also, importantly, introduces research issues in each topic area to give advanced students a small taste of research issues in OS. The lectures cover classic OS theory and emphasize the practical application of OS theory using case studies of real systems (including the teaching system). The course has a significant (50%) practical component, which is based on the teaching system OS161 from Harvard University. The assignments reinforce the practical application of OS theory by requiring students to get their hands dirty in a realistic system, implementing realistic OS components, such as processes, virtual memory, and file systems. It also forces students to get familiar with tools used in large projects, such as hierarchical Make files and a revision-control system (CVS). The course features tutorials where students discuss aspects of OS theory and the assignments. The tutorials are lead by PhD students in the field, and thus the tutorials expose students to expert and enthusiastic guidance from active researchers.

For more information about this course, click here.

Advanced Operating Systems

This runs in second term and students with strong interest in systems are encouraged to take it in third year. The course especially emphasises the practical component (which determines 65% of the final mark). Students, working in pairs, write a complete little operating system on top of seL4, starting from nothing more than a trivial seL4 example program. They are also supplied with a serial driver and a network stack. They develop a system with new device drivers, memory management (including page swapping), process management and a file system, using the supplied network stack with a Linux-based block server as an I/O device. There is a milestone each week with some required functionality which must be demonstrated working in the lab on real hardware (Arm-based single-board computers) and the implementation explained. Only the functionality requirements are given, the design is up to the students. The lectures initially cover seL4 and its API, microkernels in general, as well as a number of special topics in much greater depth and current research issues. For the final exam students are given two recent research papers and have to write a critique of them in 24 hours.

For more information about this course, click here.

Advanced Topics in Software Verification

This course aims at educating students in formal software verification. In particular, it focuses on mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade theorem provers, teaches the theoretical background to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The course is intended to bring fourth year and postgraduate students into contact with current research topics in the field of theorem proving and automated deduction and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification. Topics include higher order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs, decision procedures for a variety of logical domains, and proofs about programs. The course will provide hands-on experience with the proof assistant Isabelle/HOL. Assessment consists of 3 written assignments and a final take-home exam with Isabelle/HOL proofs and questions on the lecture material. While marks are assigned to the assignments, their primary purpose is to give concrete tasks with deadlines to help structure the learning.

For more information about this course, click here.

Distributed Systems

This course runs in third term and can be takein in third or fourth year or as a postgraduate course. It covers the system aspects of distributed systems, focusing on the main challenges encountered when designing and building distributed systems. The topics covered include: communication, replication, consistency, synchronisation, fault tolerance, security, naming, distributed objects, distributed filesystems, etc. The final exam is an open book exam and challenges students to devise solutions to typical problems faced when designing and developing specific distributed systems. The course has a strong practical component which determines 50% of the final mark. This practical component consists of two separate projects. In the first project students are asked to implement a user-level distributed shared memory (DSM) library for Linux. This project requires dealing with Unix signals and socket programming in C and implementing a simple centralised multiple-reader/ single-writer consistency protocol. The second project involves implementing a simple router network in the Erlang programming language.

For more information about this course, click here.

Modelling Concurrent Systems

This course tries to make students familiar with state-of-the-art techniques in modelling concurrent systems. This is done by comparing some of the more successful semantic models of concurrency found in the literature. The focus is on the rationale behind the design decisions underlying those models, viewed from philosophical, mathematical and computational perspectives. The course presents important background knowledge for students aiming at a scientific career in which the design of mathematical models of system behaviour is a component. It consists of lectures, weekly homework, tutorials, seminar presentations by all students, and a final exam.

For more information about this course, click here.

Algorithmic Verification

It is virtually impossible to guarantee correctness of a system, and in turn the absence of bugs by standard software engineering practice such as code review, systematic testing and good software design alone. The complexity of systems is typically too high to be manageable by informal reasoning or reasoning that is not tool supported. The formal methods community has developed various rigorous, mathematically sound techniques and tools that allow the automatic analysis of systems and software. The application of these fully automatic techniques is typically called algorithmic verification.

The course describes several automatic verification techniques, the algorithms they are based on, and the tools that support them. We discuss examples to which the techniques have been applied, and provide experience with the use of several tools.

For more information about this course, click here.