Concurrent Data Structure

Peter Hoefner, Roger Su

9 Oct 2023

24-credit only

Dependency Analysis over Stored Theorems and Proofs

Michael Norrish

9 Oct 2023

This engineering project asks the student to write code to analyse the “theory” files generated by the HOL4 system to detect redundant theorems. These are those that are never used (and might...

Finding Attacks by means of Predicate Transformers

Peter Hoefner, Michael Norrish

9 Oct 2023

Keywords: formal methods, concurrent systems, Hoare logic Unit: 24 credits

Implementing routing protocols in NS-3

Ian Shillito, Peter Hoefner

9 Oct 2023

Keywords: routing protocol, network, network simulator, programming. Units: 12 units

Mechanisation of the milli Common Representation Language

Peter Hoefner, Chun Tian

9 Oct 2023

Keywords: process algebra, Isabelle/HOL, proof mechanisation Units: 24 units

Mechanised Graph Theory

Michael Norrish, Chun Tian

9 Oct 2023

Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Graph Theory Units: 12/24 units

Mechanised Mathematics

Michael Norrish

9 Oct 2023

Mechanising mathematics is the task of turning (relatively) well-understood mathematics into verified proofs with an interactive theorem-proving system. Such verified material can then lie behind high-assurance software.

Modelling, Analysing and Verifying Routing Protocols

Peter Hoefner, Ian Shillito

9 Oct 2023

Keywords: process algebra, formal modelling, formal methods Units: 12/24 units

Unit-Testing a Parser

Peter Hoefner

9 Oct 2023

In the past , we have developed a parser for a formal language, called AWN, which features a formal syntax and formal semantics. The parser is written in Scala, using the processing...

User-Friendly IDE for the language AWN

Peter Hoefner, Roger Su

9 Oct 2023

The techniques we use for modelling, analysing and verifying routing and communication protocols are based on the simple programming language AWN, which offers expressions for (arbitrary) data structures and basic primitives, such...

Verifying Elements of Algorithmic Graph Theory

Peter Hoefner, Roger Su

9 Oct 2023

Keywords: relation algebra, verification, graph algorithms, proof mechanisation Units: 12/24 units

Verifying Indentation Sensitive Parsing

Michael Norrish

9 Oct 2023

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...

Mechanised Probability Theory - Ergodic Theory

Chun Tian

10 Oct 2023

Keywords: Probability Theory, HOL4, Interactive Theorem Proving, Proof Mechanisation Units: 12 units

Cut Elimination of Lambek Calculus (Categorial Grammar)

Chun Tian, Ian Shillito

11 Oct 2023

Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, NLP Units: 12/24 units

Mechanised Cryptography

Chun Tian

11 Oct 2023

Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Cryptography Units: 12/24 units

Mechanised Graph Theory - Advanced Topics

Chun Tian, Michael Norrish

11 Oct 2023

Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Graph Theory Units: 24 units

The Edinburgh Concurrency Workbench in HOL4

Chun Tian

11 Oct 2023

Keywords: Interactive Theorem Proving, Proof Mechanisation, Higher Order Logic, Concurrency Theory Units: 24 units

Executable Process Algebras

Peter Hoefner, Fabian Muehlboeck

13 Oct 2023

Process Algebras (or Process Calculi) are a diverse family of related approaches for formally modelling concurrent, distributed and parallel systems. Theyi provide a tool for the high-level description of interactions, communications, and synchronizations...

Reasonable Fairness Assumptions for Mutual Exclusion Protocol

Roger Su, Peter Hoefner

13 Oct 2023

Keywords: transition system, formal reasoning, liveness properties Units: 24 units

Representation Learning for Multi-View Graphs

Qing Wang

18 Oct 2023

Real-world graphs often exist with multiple views, where each view describes a distinct type of interaction among a shared set of vertices. For example, in social networks, interactions between individuals include friendships,...

Creating a spatial intelligent musical instrument in augmented reality

Charles Martin

18 Oct 2023

Creating a physical intelligent musical instrument with the Bela single-board computer

Charles Martin

18 Oct 2023

AI models for guiding collaborative performance

Charles Martin

18 Oct 2023

A web interface for creating musical AI systems

Charles Martin

18 Oct 2023

Compiling CakeML to WASM

Michael Norrish

2 Nov 2023

The WASM (“Web Assembly”) language is an important low-level language because of its widespread availability inside the world’s deployed browsers.

Implementing a Semantics for Pipelining in Racket

Roger Su, Peter Hoefner, Fabian Muehlboeck

4 Nov 2023

Keywords: Concurrency; operational semantics; memory models Units: 12/24 units

[$10K Scholarship for domestic Honours] Investigating the Manipulative Power of Large Language Models using Social Deduction ...

Penny Kyburz

17 Nov 2023

$10K stipend, $5K training allowance, apply by 7 January

[$10K Scholarship for domestic Honours] Justice in the Metaverse

Penny Kyburz

17 Nov 2023

$10K stipend, $5K training allowance, apply by 7 January

Monotone tense logic

Jim de Groot, Ian Shillito

17 Nov 2023

The logic of time is a subfield of logic that is of interest to philosophers, computer scientists and mathematicians alike. It played an important role in the development of modal logic, and...

Software Innovation in Data Science

Graham Williams

20 Nov 2023

Artifact-based projects building your software engineering skills for artificial intelligence.

Approximate solutions and preconditioning using AMX, AVX and Tensor Cores

Rhys Hawkins

28 Nov 2023

This project is intended as a full year Honours project and a scholarship is available to the right candidate.

Algorithms in Robotics for Task and Motion Planning

Rahul Shome

30 Nov 2023

Computational problems in robotic planning and decision-making.

Applying machine learning to neuroimaging data to improve diagnosis of depression and ADHD

Hanna Suominen

30 Nov 2023

ADHD, Depression, Machine Learning, Neuroimaging, Neuroinformatics, Applications to Health and Medicine

Applying machine learning to neuroimaging data to improve our understanding of healthy cognitive function

Hanna Suominen

30 Nov 2023

Cognitive Function, Machine Learning, Neuroimaging, Neuroinformatics, Applications to Health and Medicine

Applying machine learning to neuroimaging data to predict depression treatment response so patients get the right treatment f...

Hanna Suominen

30 Nov 2023

Depression, Machine Learning, Neuroimaging, Neuroinformatics, Applications to Health and Medicine

Story planning: unlimiting creativity

Patrik Haslum, Hanna Suominen

30 Nov 2023

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 validation and presentation of policies for MDPs

Patrik Haslum

1 Dec 2023

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 Dec 2023

“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,...

Adaptive Mesh Refinement for Spectral Element problems

Rhys Hawkins

7 Dec 2023

This project is intended as a full year Honours project and a scholarship is available to the right candidate.

Iterative approaches to the solution of large scale non-linear eigen problems.

Rhys Hawkins

7 Dec 2023

This project is intended as a full year Honours project and a scholarship is available to the right candidate.

High Performance Digital Twins for Type 1 Diabetes Research

Chirath Hettiarachchi

14 Dec 2023

Engineering a GPU-based simulator to advance research & development in Reinforcement Learning (RL)-based Artificial Pancreas Systems.

Machine Learning for Bio-marker Discovery & Modelling in Type 1 Diabetes

Chirath Hettiarachchi

14 Dec 2023

Analyzing physiological signals to identify biomarkers associated with exercise in Type 1 Diabetes.

Reinforcement Learning (RL) Agents for Glucose Regulation

Chirath Hettiarachchi

14 Dec 2023

Exploring and Implementing State-of-the-art RL algorithms to design a glucose control system for Type 1 Diabetes.

Machine learning for precision medicine through cytometry and genomic applications

20 Dec 2023

Machine learning for precision medicine through cytometry and genomic applications

StabilitySort: pathogenic mutation community detection with graphs

20 Dec 2023

Supervisor: Dan Andrews (Jubilee Joint Fellow, CECC & JCSMR; Dan.Andrews@anu.edu.au)

A Deep Learning Approach to Fusion of Multimodal Biomedical Data

21 Dec 2023

Supervisor: Dr. Ben Mashford (CECC & JCSMR)

Accelerating biological sequence alignment algorithms

Thang Bui

23 Dec 2023

A DNA sequence is the information system that encodes all life 1. Multiple scientific disciplines (e.g. medicine, public health, genetic epidemiology) rely on genomic data 2. The value of DNA sequences arises...

Applying geometry and machine learning to detect genes in DNA sequences

Thang Bui

23 Dec 2023

A DNA sequence is the information system that encodes all life 1. Multiple scientific disciplines (e.g. medicine, public health, genetic epidemiology) rely on genomic data 2. The value of DNA sequences arises...

DNA divergence models that are less crazy

Thang Bui

23 Dec 2023

A DNA sequence is the information system that encodes all life 1. Multiple scientific disciplines (e.g. medicine, public health, genetic epidemiology) rely on genomic data 2. The value of DNA sequences arises...

PhD Scholarship: Verification of Safety-critical Systems using Rely/Guarantee

Nisansala Yatapanage

23 Dec 2023

Safety-critical systems include systems such as air-traffic control, railway and industrial systems. The critical aspect of these systems is that if something goes wrong, human lives would be in danger. For this...

Privacy-Preserving Perception for Robotics

Yunzhong Hou, Dylan Campbell, Rahul Shome

28 Jan 2024

Building a robotic vision system that avoids collecting privacy-sensitive data (e.g. faces or licence plates) while perceiving the world.

Making robots play music

Charles Martin, Rahul Shome

9 Feb 2024

This project is in the field of musical robotics, an area where researchers consider the many difficulties involved in teaching robots to play musical instruments by themselves, in groups, or in collaboration...

Responsible AI Research Projects @ANU-Xiaoyu Sun

Xiaoyu Sun

12 Feb 2024

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 these...

Model-Heterogeneous Federated Learning

Amanda Barnard AM

15 Feb 2024

Federated Learning is a new paradigm of distributed machine learning that enables multiple clients with private data to collaboratively build a high-performance prediction model. In federated learning, the training process is coordinated...

Ultra-fast Photonic Computing for Deep Learning Acceleration

Amanda Barnard AM

15 Feb 2024

Large-scale deep learning models with millions and even billions of parameters are commonly used to achieve exceptional performance. However, training such models on existing electronic hardware such as GPU can take anywhere...

Usability Study of Modules for CUE Configuration Language

20 Feb 2024

Please contact Alex Potanin (alex.potanin@anu.edu.au) for a project that involves a usability study of CUE language users to help design the new generation of module and package system.