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
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,...
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...
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
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...
Accelerated Satisfaction
Charles Gretton
11 Feb 2026
SAT and #SAT solving in modern heterogeneous HPC environments, making use of GPUs and other accelerators to improve overall scalability and performance. Co-supervised with Dr Cody Christopher.
Discovering Subproblems in SAT and #SAT using HPC
Charles Gretton
11 Feb 2026
Boolean SAT(isfiability) and the related “counting” #SAT problem can be slow to solve on a serial computer. Use distributed HPC to cut formulae up into smaller pieces, so that search can then...
Satisfaction can be Relaxing
Charles Gretton
11 Feb 2026
Revisit, review, and evaluate semi-definite programming (SDP) relaxations of the Boolean SAT problem. Co-supervised with Dr Cody Christopher.
Transformers for Ramsey Colorings
Charles Gretton
11 Feb 2026
“go big or go home”. This project will be co-supervised with Dr Cody Christopher.
PDE Discovery of Force Balance in Toroidal Magnetic Confinement
Matthew Hole
13 Feb 2026
Deep learning of mathematics in fusion energy science
Cognitive fatigue and reduced attention in a medium-fidelity driving simulator
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein, Ms Amany Al Luhaybi and Dr Yonghui Liu.
LLM-driven persuasion on climate claims with biosignals
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein and Dr Yonghui Liu.
Personality preditions from text, wearables and video
18 Feb 2026
This project will be supervised by Prof Tom Gedeon (tom.gedeon@anu.edu.au), Dr Zakir Hossein and Dr Yonghui Liu
Planning Meets LLMs
Sylvie Thiébaux
19 Feb 2026
Background
Breaking Cryptography
Thomas Haines
20 Feb 2026
Cryptography is widely used in many protocols but rarely implemented by someone with a clear idea of what they were doing.
Privacy First Data Science and AI
Graham Williams
20 Feb 2026
Graham Williams
Proving Cryptography
Thomas Haines
20 Feb 2026
Cryptography is widely used in many protocols but rarely implemented by someone with a clear idea of what they were doing.
Creating a spatial intelligent musical instrument in augmented reality
Charles Martin
20 Feb 2026
The idea of this project is to develop new kinds of musical instruments for augmented reality headsets.
Intelligent musical instrument projects with IMPSy
Charles Martin
20 Feb 2026
The idea of this project is to develop new kinds of intelligent musical instruments and platforms for designing them.
Projects in Automated Planning
Pascal Bercher
21 Feb 2026
This is basically a “dummy project announcement” to help you find projects!
Responsible AI Research Projects @ANU-Xiaoyu Sun
Xiaoyu Sun
9 Mar 2026
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...
Verifying Quantum Error Correction with Topological Connectivity Reasoning
Alex Potanin
15 Apr 2026
Prerequisites: Strong programming skills; ideally familiarity with quantum computing fundamentals; interest in programming languages and/or formal verification. Experience with proof assistants (ideally Rocq) is a plus, but not required.