Skip to main content

Courses

The University of New South Wales

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 (UNSW)

Normally taken in first semester 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 (UNSW)

This runs in second session 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 L4, starting from nothing more than a trivial L4 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. The development environment is presently a MIPS simulator (Sulima, developed by one of our students and used for all MIPS-based work in our lab). There is a milestone each week with some required functionality which must be demonstrated working in the lab on real hardware (locally-developed MIPS-based computers) and the implementation explained. Only the functionality requirements are given, the design is up to the students. The lectures initially cover L4 and its API, then microkernels in general, then move on to cover a number of special topics in much greater depth than COMP3231, as well as a number of 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 (UNSW)

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 (UNSW)

This course is taken as an elective in 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 (UNSW)

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 (UNSW)

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.

Overview of Logic and Computation (ANU)

(Mathematical) logic has been called the 'Calculus of Computer Science' and it is the main theoretical tool to describe computation. Implemented systems for logical reasoning are routinely used by industry today, e.g., for software and hardware verification. The rationale behind this course is that understanding the concepts of logic and computation is a valuable preparation for further studies in theoretical computer science and its application in the real world.

The course focuses on questions of bringing logic to computer. It covers important logics that can successfully be implemented on computer: propositional logic, first-order logic and certain temporal logics. The latter is used for verification of dynamic properties of reactive systems (an operating system is an example for such a system). It is a special case of a so-called modal logic, a family of logics that are, in their full generality, much richer than the above mentioned logics. Modal logics are covered as well.

For more information about this course click here.

Foundations of Mathematics (ANU)

This is an honours-stream course in the ANU's maths department. Its focus is the fundamentals that lie beneath all of mathematics. In particular, students learn about formal logic (propositional and predicate), and how these tools can then be used to formalise the rest of mathematics. This formalisation is based on the von Neumann-Bernays-Gödel axiomatisation of set theory. In addition to showing how mathematical constructions such as number can be performed in set theory, the course also looks at transfinite arithmetic with ordinals and cardinals. Finally, the course concludes with an introduction to computability theory and Gödl's famous incompleteness theorem.

For more information about this course, click here.

Theory of Computation (ANU)

This course gives an introduction to various models of computation, ranging from finite automata for describing formal languages to Turing machines for describing general purpose programs. Moreover, the Turing machine model of computation is at the heart of the theory of computational complexity, and as such essential to almost all areas of computer science.

The individual topics covered in this course include: regular and context-free languages; finite automata and pushdown automata; Turing machines; Church's thesis; computability - halting problem, solvable and unsolvable problems; space and time complexity; classes P, NP and PSPACE; NP-Completeness.

For more information about this course, click here.

Served by Apache on Linux on seL4.