Generalization in Imitation Learning
Hanna Kurniawati
14 Aug 2025
This is a one year project to investigate how Partially Observable Markov Decision Processes (POMDPs) could help improve generalisability in imitation learning. We will seek to integrate some of our new approximate...
[Domestic PhD scholarship] Towards Trustworthy Multi-Agent AI Systems: From Individual to Collective Reliability
Penny Kyburz
8 Oct 2025
$43,333 stipend plus training, cost of living, and travel allowances, includes placement with Gradient Institute
Implementing a Semantics for Pipelining in Racket
Roger Su, Peter Hoefner, Fabian Muehlboeck
24 Oct 2025
Keywords: Concurrency; operational semantics; memory models Units: 12/24 units
Is the Rely-Guarantee Method Relative Complete?
Peter Hoefner
24 Oct 2025
Keywords: Concurrency; structural operational semantics; verification Units: 12/24 units
Modelling, Analysing and Verifying Routing Protocols
Peter Hoefner, Roger Su
24 Oct 2025
Keywords: process algebra, formal modelling, formal methods Units: 12/24 units
Predicting Student Enrolment Numbers
Peter Hoefner, Bernardo Nunes
24 Oct 2025
(6+6 project only)
Reasonable Fairness Assumptions for Mutual Exclusion Protocol
Roger Su, Peter Hoefner
24 Oct 2025
Keywords: transition system, formal reasoning, liveness properties Units: 24 units
Verifying Algorithms Using Cooperative Methods
Peter Hoefner
24 Oct 2025
Units: 12 (6+6) or 24 (Honours)
A structural editor for proofs and inference rules
Liam O'Connor
27 Oct 2025
Structural editing (such as seen in the programming language Hazel https://hazel.org) is a powerful idea where the language is integrated with the editor, making it impossible to even *input* illegal programs. The...
Formally Verified Raster Drawing Algorithms
Liam O'Connor
27 Oct 2025
Raster drawing algorithms are algorithms that render continuous geometric shapes (lines, circles, curves) in a discrete 2D pixel space. Examples include Bresenham’s line drawing and circle drawing algorithms. These algorithms are intricate,...
Formally Verifying Automata Learning
Liam O'Connor
27 Oct 2025
Automata Learning algorithms such as Angluin’s L* have been widely used in the testing and specification inference communities. Yet, the correctness of these algorithms has not yet been formally established by mechanised...
Mechanising Linear Temporal Properties in Lean
Liam O'Connor
27 Oct 2025
The theory of linear temporal properties – sets of system behaviours – including safety and liveness properties, as well as those described by linear temporal logics, is now well studied with many...
Multi-modal Learning for Next Generation Quantum Sensors
Amanda Barnard AM
5 Nov 2025
Collaborate on a real-world project using contrasive deep learning and eXplainable AI to develop next generation quantum sensors.
Compiling CakeML to WASM
Michael Norrish
11 Nov 2025
The WASM (“Web Assembly”) language is an important low-level language because of its widespread availability inside the world’s deployed browsers.
Verified JSON Parsing in CakeML
Michael Norrish
11 Nov 2025
JSON parsing is a standard and important facility used in many programming languages. This project requires the student to implement verified JSON-parsing for the CakeML programming language.
Verifying Indentation Sensitive Parsing
Michael Norrish
11 Nov 2025
Programming languages such as Haskell and Python (and the YAML notation) depend on whitespace as part of indentation to determine their syntax. The specification of this syntax is quite ugly, and very...
Automatic generation of POMDP models
Hanna Kurniawati
1 Dec 2025
This project will investigate automatic model generation of one of the most general frameworks for sequential decision-making under uncertainty, namely the Partially Observable Markov Decision Processes (POMDPs). Specifically, we will investigate how...
Robot navigation through crowds
Hanna Kurniawati
1 Dec 2025
Interested in having an autonomous robot helper in conferences/events, such as Open Day, Christmas Party, etc.? This might be the project for you!
Exploring dependent types for matrix representations
Liam O'Connor, Peter Hoefner
11 Dec 2025
Background: Dexter Kozen’s famous completeness theorem for Kleene algebras relies on a fairly intricate proof that n*n matrices over a Kleene algebra are themselves a Kleene algebra. The proof relies on an...
Understanding the Limits of LLMs on Graph Problems
Ahad N. Zehmakan, Jing Jiang
11 Dec 2025
Background
Responsible AI Research Projects @ANU-Xiaoyu Sun
Xiaoyu Sun
18 Dec 2025
We are seeking highly motivated Honours/Master students to work on the following research projects to progress responsible AI research. Opportunity for a further PhD study is possible depending on student’s performance in...
Efficient validation and presentation of policies for MDPs
Patrik Haslum
1 Jan 2026
The Markov Decision Process (MDP) is the canonical model of a sequential decision-making problem under uncertainty, and is solved by probabilistic AI planning methods. The solution to an MDP is a policy:...
Optimal troubleshooting (and other tractable POMDPs)
Patrik Haslum
1 Jan 2026
“Troubleshooting” is the problem of integrated active diagnosis and repair, in which the repairer must repeatedly select between (imperfect) diagnostic tests and repairs to perform to restore functionality of a faulty system,...
Quantum Computing Verification
Alex Potanin
1 Jan 2026
I am looking for undergraduate and postgraduate research project students (e.g. 6 unit ASC projects, 12 unit research projects, or 24 unit honours projects) to work on many aspects of Quantum Computing...
Rust Borrow Checker
Alex Potanin
1 Jan 2026
Rust’s ownership- and borrowing-based type system enables strong guarantees such as memory safety and data-race freedom. However, these guarantees sometimes force programmers into patterns that can make code less clear or more...
Software Verification with Lean
Alex Potanin
1 Jan 2026
I am interested in pushing the boundaries of what is possible in software verification as inspired by the recent advances, such as the Loom verification framework (https://ilyasergey.net/publications/) within Lean. If you are...
Story planning: unlimiting creativity
Patrik Haslum, Hanna Suominen
1 Jan 2026
The plot (or narrative) of a story has some similarity with a plan, as it is usually defined in classical AI planning. This has led researchers to investigate planning-based approaches to automatic...
Efficient High-dimensional Vector Search
Mengxuan Zhang
8 Jan 2026
The embedding of unstructured data, e.g., text, image, audio, as high-dimensional vectors, is an emerging and popular way to represent, manage and utilize the data from diverse sources. The storage of such...
Graded and Guarded Modal Types: Cost Analysis for Non-Terminating Programs
Ranald Clouston
15 Jan 2026
Type systems can provide static guarantees about the behaviour of all possible programs written in a language. This project involves the combination of two recent advances in type theory: graded and guarded...
Auto-verification of an embedded system application
Yan Liu, Peter Hoefner
16 Jan 2026
Keywords: model checking, timed automata, process algebra, computation tree logic, compilation
Integrate Fiducia with MicroKit - Transpiler to SDF
Yan Liu, Alex Potanin
16 Jan 2026
Keywords: programming language design and implementation, embedded system development Units: 12 units
Axiomatic Geometry in Isabelle/HOL
Peter Hoefner
22 Jan 2026
This project aims to mechanise axiomatic geometry in Isabelle/HOL, providing a machine-checked formalisation of elementary Euclidean geometry based on Tarski-style axioms. The goal is to obtain a trustworthy, reusable foundation for geometric...