Taste of Research Summer Scholarships

2026 Projects - School of Computer Science and Engineering

Computer Science & Engineering Research Areas

Related Projects

 

Computer Science & Engineering Projects

 

No School Research Area


Project Title: Agentic Sensor Language Models for Reasoning over Time-Series
Name of Supervisor: Flora Salim
Email of Supervisor: flora.salim@unsw.edu.au
Name of Joint/Co-Supervisor: Hao Xue; Zechen Li
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Recent efforts applying LLMs for time-series analysis and classification tasks, typically by converting time-series signals to text or images to be processed by LLMs or VLMs, suffer from poor performance and lack of interpretability. We have pushed the boundaries of using LLMs for time-series classification through SensorLLM and ZARA. In Sensor LLM, we introduced a two-stage framework—first aligning sensor data with intuitive trend descriptions, then fine-tuning for classification—achieving accuracy on par with or surpassing state-of-the-art supervised models. In contrast, ZARA eliminates retraining altogether, proposing an agent-based, zero-shot framework that combines a feature knowledge base, evidence retrieval, and hierarchical reasoning to predict activities while also providing natural-language explanations. While SensorLLM highlights generalization through human-intuitive alignment and supervised finetuning, ZARA emphasizes interpretability and plug-and-play adaptability, achieving strong zero-shot performance and explainability.

This Taste of Research project will build on our past research. The focus of the project is on verifiable reasoning, since most current reasoning/thinking lacks explicit evidence support. The overarching goal is to enhance time-series reasoning capabilities over a broad time-series tasks, enabling robust QA and chat-based exploration over high dimensional time-series.
Research Environment: The ToR is embedded in the Cruise Research group. We're one of the world leading group in machine learning for multimodal sensors, time-series and spatio-temporal data, and AI for ubiquitous computing, urban computing, and geospatial computing. Flora Salim is a Vice Chair of the IEEE Task Force on AI for Time-Series and Spatio-Temporal Data. Check our group website: https://cruiseresearchgroup.github.io
Novelty and Contribution: .
Expected Outcomes: A publishable research output and a working front-end / web-based demo.
Reference Material Links: 1. Li, Z., Deldari, S., Chen, L., Xue, H. and Salim, F.D., 2024. SensorLLM: Human-Intuitive Alignment of Multivariate Sensor Data with LLMs for Activity Recognition. arXiv preprint arXiv:2410.10624. https://arxiv.org/abs/2410.10624

2. Li, Z., Chen, B., Xue, H. and Salim, F.D., 2025. ZARA: Zero-shot Motion Time-Series Analysis via Knowledge and Retrieval Driven LLM Agents. arXiv preprint arXiv:2508.04038. https://arxiv.org/abs/2508.04038

3. Yang, R., Xue, H., Razzak, I., Hacid, H. and Salim, F.D., 2025. Beyond Single Pass, Looping Through Time: KG-IRAG with Iterative Knowledge Retrieval. arXiv preprint arXiv:2503.14234. https://arxiv.org/abs/2503.14234
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Auto-translation of C programs to Pancake
Name of Supervisor: Ivan Velickovic
Email of Supervisor: i.velickovic@unsw.edu.au
Name of Joint/Co-Supervisor: Miki Tanaka
Email of Joint/Co-Supervisor: miki.tanaka@unsw.edu.au
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Pancake is a research programming language currently under development at Chalmers University of Technology, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.
Pancake is intended to be used for low-level programming, such as device drivers. It is similar to C, but is significantly simpler. While this makes it easier to verify Pancake programs, it means that writing or porting existing components to Pancake can be time-consuming.
This project aims to create a tool to automatically translate C code into a Pancake program that we would then either manually edit or directly do formal verification on.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: 1. Report outlining the approach taken, tradeoffs considered and work done;
2. Pull request to the Trustworthy Systems Group's github repository with implementations.
Reference Material Links: https://trustworthy.systems/projects/pancake
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Behaviour trees for teams of robots
Name of Supervisor: Oliver Obst
Email of Supervisor: o.obst@unsw.edu.au
Name of Joint/Co-Supervisor: .
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Intelligent & Autonomous Systems
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Behaviour trees are widely used to control decision-making in systems ranging from NPCs in computer games to robots in warehouses, where they provide a structured and interpretable way to organise behaviour.

muesli-bt is an open-source project at UNSW that provides a compact and efficient behaviour tree runtime with support for bounded-time planning, asynchronous actions, and integration with vision-language-action models, simulation, and robotic systems.

In this project, you will develop a lightweight multi-agent coordination layer for muesli-bt to allow multiple robots to run independent behaviour trees while coordinating through shared task state. This coordination is relevant to industrial robotics, such as warehouse automation and multi-robot task allocation. The project will evaluate how this approach supports decentralised team behaviour in such scenarios without relying on a central planner.
Research Environment: This project will be collaborative across our robotics projects involving academics and research students. The project offers experience in robotics software, and experimental testing of software on robots.
Novelty and Contribution: .
Expected Outcomes: Expected outcome is a developed and tested approach for multiple robots to coordinate while each robot is running its own behaviour tree. This should include a working software prototype, trials in simulation or on robots where possible.
Reference Material Links: https://github.com/unswei/muesli-bt
and
https://github.com/unswei/muesli-studio
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Better debugging tools for LionsOS
Name of Supervisor: Ivan Velickovic
Email of Supervisor: gernot@unsw.edu.au
Name of Joint/Co-Supervisor: Julia Vassiliki
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Embedded Systems and Communications
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: LionsOS is a new seL4-based OS for embedded systems under development at TS. LionsOS isolates programs more than conventional Operating Systems and relies a lot more on asynchronous communication. Current tools used for debugging on conventional OSes are more limited for our use case.
Current tools such as GDB are not equipped to debug our kind of architecture and so certain bugs that happen between process boundaries or rely on the scheduling of a system can be difficult to catch and fix.
This project is to explore other ways of debugging system-wide execution such as scheduling and inter-process communication. This will involve looking at more modern tools such as rr as well as tracing infrastructure available in other OSes.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: 1. Port of an existing or development of a new tracing framework to give us more introspection into systems built on LionsOS.
2. Evaluation of the feasibility of a record-and-replay debugger, such as RR.
Reference Material Links: https://sel4.systems/
https://trustworthy.systems/projects/LionsOS/
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Building Agentic Bug Bounty Hunter with n8n
Name of Supervisor: Yueakng Li
Email of Supervisor: yuekang.li@unsw.edu.au
Name of Joint/Co-Supervisor: .
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: The project aims to build an automated agentic workflow to automatically create PR or issues for submitting bugs/vulnerabilities to open-source projects and discuss with the project maintainers/developers.

This project provides an opportunity to work with a team of security experts who have rich experience in bug hunting.
Research Environment: Linux or MacOs.
Novelty and Contribution: .
Expected Outcomes: A tool that can help to automate the post-detection work for bug hunting.
Reference Material Links: https://www.anthropic.com/news/claude-code-security
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Building trusted agentic systems from untrusted LLMs
Name of Supervisor: Vineet Rajani
Email of Supervisor: v.rajani@unsw.edu.au
Name of Joint/Co-Supervisor: Arash Shaghaghi
Email of Joint/Co-Supervisor: a.shaghaghi@unsw.edu.au
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Intelligent & Autonomous Systems
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: The transition from passive Large Language Models (LLMs) to Agentic AI systems capable of autonomous reasoning, tool use, and environmental interaction marks a significant shift in the artificial intelligence landscape. While these agents offer transformative potential for productivity and complex problem-solving, they introduce a novel attack surface and unique safety challenges that traditional AI frameworks are ill-equipped to handle. This project will 1) explore the state-of-the-art methods in of building trustworthy agentic AI, and 2) Implement a prototype domain specific language which will only allow implementation of trustworthy agentic workflows over untrustworthy LLMs.
Research Environment: The selected student will get an opportunity to closely work with researchers having expertise in formal methods, cybersecurity and AI.
Novelty and Contribution: .
Expected Outcomes: A language-based framework for writing agentic systems that can be provably trusted.
Reference Material Links: https://arxiv.org/pdf/2602.16708
https://arxiv.org/pdf/2512.01295
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Delegated Autonomy, Real Security: Authorization for AI Agents in IoT & Multi?Agent Systems
Name of Supervisor: Arash Shaghaghi
Email of Supervisor: a.shaghaghi@unsw.edu.au
Name of Joint/Co-Supervisor: Yvo Desmedt
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Intelligent & Autonomous Systems
Applicable to other Engineering
schools/disciplines:
Terms:
Abstract: Autonomous AI agents are quickly moving from “nice-to-have assistants” to real actors in the world. They can book travel, manage accounts, coordinate workflows, and interact directly with IoT devices and edge services in real time. That shift raises a tough security question: **how do we delegate authority to an AI agent in a way that’s explicit and transparent, keeps humans in control, and still stays lightweight and privacy-preserving?**

This project targets a clear gap. Most Identity and Access Management (IAM) systems were built for long-lived users and stable services. They weren’t designed for AI agents that might exist only for a single task, use multiple tools, and make decisions based on context. In practice, agents can appear briefly and vanish once the job is done, jump across different tools and organisations to complete a workflow, collaborate with other agents in multi-agent settings, and operate at the edge where compute is limited and connectivity can be unreliable.

Research on agentic authorization keeps running into the same issues: delegation across multiple entities is clunky, context is hard to capture and enforce, and token or session management doesn’t scale well when hundreds or thousands of agents interact with many services and devices.

Your role in this project is to help design and prototype principled access-control mechanisms tailored for delegated AI agents at the edge. The goal is to give people clear, meaningful control over permissions, identity, and accountability, while ensuring the system can reliably enforce those choices.

You’ll be working with a research team developing innovative solutions in this space.
Research Environment: Joint project with academics from the University of Texas at Dallas. The student will work with a team of researchers working on the topic, including a PhD student.
Novelty and Contribution: .
Expected Outcomes: Research paper and contribution to a patent
Reference Material Links: Available on request
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Deployable firewall based on seL4
Name of Supervisor: Courtney Darville
Email of Supervisor: gernot@unsw.edu.au
Name of Joint/Co-Supervisor: Peter Chubb
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Embedded Systems and Communications
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: The TS group has just developed a proof-of-concept of a secure network firewall running on the verified seL4 microkernel and LionsOS. Currently the firewall supports the transmission of traffic between two network interfaces, and is able to apply simple filtering rules to a subset of IP traffic (TCP, UDP, ICMP). Filtering rules and forwarding routes may be viewed and updated through a rudimentary web interface. Presently it has a number of missing features that prevent its practical use, with each feature requiring a varying degree of work to implement. While we are happy to leave most of them to the open-source community, we are looking for interns for the higher priority ones. These are:
* Support for IPv6, as well as more IP protocols and ethernet types
* A collection of optimised, concurrency-safe data structures which can be used by firewall components for reading and updating shared network state (e.g. NAT port mappings, TCP connection)
If there is sufficient time left after the above, the rest can be spent on improvements to existing features or adding further functionality, with the ultimate aim of enabling the firewall to be deployed on the TS network.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: 1. functional firewall that can be deployed
2. report describing design and implementation.
Reference Material Links: https://sel4.systems/
https://trustworthy.systems/projects/LionsOS/
https://lionsos.org/docs/examples/firewall/contributing/
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Formalising and verifying device controllers
Name of Supervisor: Miki Tanaka
Email of Supervisor: miki.tanaka@unsw.edu.au
Name of Joint/Co-Supervisor: Hammond Pearce, Gernot Heiser
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Embedded Systems and Communications
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: The Trustworthy Systems (TS) group is working on verifying device drivers for LionsOS using the Pancake language. This work is inevitably dependent on a correct formalisation of the HW interface.

We have established a workflow to take an open-source hardware designs of device controllers (from the OpenTitan project, for example) and formalise its software interface in the theorem prover HOL4. We then validate the formalised model against the origial hardware design by showing the equivalence/refinement between them.

The project is to apply this workflow to produce more use cases, possibly by taking part in the on-going formalisation of devices such as I2C and SPI.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: • Report outlining the approach taken, tradeoffs considered and work done.
- Pull request to the Trustworthy Systems Group's github repository with formalization and proofs.
Reference Material Links: https://trustworthy.systems/projects/LionsOS/
https://trustworthy.systems/projects/pancake/
https://hol-theorem-prover.org/
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Grounding LLMs with Ontologies: Linking, Reasoning, and Beyond
Name of Supervisor: Jianwei Wang
Email of Supervisor: jianwei.wang1@unsw.edu.au
Name of Joint/Co-Supervisor: Wenjie Zhang
Email of Joint/Co-Supervisor: wenjie.zhang@unsw.edu.au
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Intelligent & Autonomous Systems
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Large language models can generate impressive responses, but they sometimes produce incorrect or inconsistent information because they lack explicit grounding in structured knowledge. Ontologies provide a way to organize knowledge about concepts and their relationships, which can help AI systems better understand and reason about information.

In this project, the student will work with a senior researcher and join a small research team comprising postgraduate students. Together, the team will explore how large language models can connect their generated text to concepts in an ontology and use these structured relationships to support more reliable reasoning.

The aim of the project is to investigate simple methods for linking language model outputs to ontology concepts and to study how ontology-based reasoning can improve the accuracy and consistency of AI systems. Through this work, the student will gain hands-on experience in modern AI research and knowledge-driven approaches to intelligent systems.
Research Environment: The student will work closely with a senior researcher and collaborate with a small team of postgraduate students working on AI and data-centric systems.

The supervisor will provide the relevant research environment, including GPU server and LLM API.
Novelty and Contribution: .
Expected Outcomes: The project will produce an experimental study on ontology linking and ontology-based reasoning with large language models. Outcomes include a research poster, a short research report, and a project presentation. There may also be opportunities to contribute to a conference submission and to participate in the academic review process.
Reference Material Links: https://github.com/weAIDB/awesome-data-llm
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: PainPoint – Gaze-Based Communication for Nonverbal ICU Patients
Name of Supervisor: Ali Darejeh
Email of Supervisor: ali.darejeh@unsw.edu.au
Name of Joint/Co-Supervisor: Eye Gaze company
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Immersive Systems and Virtual Reality
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Please refer to project information on the Faculty Taste of Research - Advertised Taste of Research areas:

https://www.unsw.edu.au/engineering/student-life/undergraduate-research-opportunities/advertised-taste-research-areas
Research Environment: CSE VR lab
Novelty and Contribution: .
Expected Outcomes: This project will:
• Demonstrate feasibility of gaze-based medical communication
• Improve care for nonverbal and vulnerable patients
• Enable faster and more accurate clinical decision-making
• Lay the foundation for a broader communication platform (EyeVoice)
• Contribute to research in human-computer interaction, healthcare technology, and assistive systems
Reference Material Links: https://unsw-my.sharepoint.com/:w:/g/personal/z5081642_ad_unsw_edu_au/IQDOHHrc-Y-5T6_J4Gf_DVD0AZCR5SxvTX3feKukrbsHRmw?e=uQnSEH
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Pancake-to-Viper transpiler refactor
Name of Supervisor: Miki Tanaka
Email of Supervisor: miki.tanaka@unsw.edu.au
Name of Joint/Co-Supervisor: Gernot Heiser
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Pancake is a research programming language for systems programming developed at Chalmers University of Technology, ANU, and UNSW. It is implemented in the theorem prover HOL4 and comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification.

We have a prototype transpiler that translates annotated Pancake programs into Viper, which we then feed to SMT-backends for verification. We have used this framework to verify an Ethernet driver. In order to improve the guarantee that the framework provides, we plan to verify the correctness of the transpiler itself.

The project is to refactor and reimplement this transpiler to make it more amenable to verification. Specifically, we aim to reimplement it either in CakeML or directly in the theorem prover HOL4 (it is currently implemented in Rust), to improve its parsing phase, and to remove dependency on an external tool.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: - Report outlining the approach taken, tradeoffs considered and work done.
- Pull request to the Trustworthy Systems Group's github repository with implementations.
Reference Material Links: https://trustworthy.systems/projects/pancake/
https://www.pm.inf.ethz.ch/research/viper.html
https://cakeml.org/
https://hol-theorem-prover.org/
https://arxiv.org/abs/2501.08249
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Process Mining for Curricular Pathway Analysis: A Case Study Using UNSW's Master of Information Tech
Name of Supervisor: Dr Rachid Hamadi
Email of Supervisor: r.hamadi@unsw.edu.au
Name of Joint/Co-Supervisor: .
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Education
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: This project explores how process mining can be applied to understand and improve student progression pathways through university curricula. Using Celonis, a leading process mining platform, the project will analyse enrolment and performance data from the UNSW Master of Information Technology (MIT, program 8543) as a case study.

Students often follow diverse journeys through a program, influenced by prerequisites, course availability, and personal choices. By transforming academic records into event logs and applying process mining techniques, this project aims to uncover actual progression patterns, identify bottlenecks (e.g., frequently repeated courses or delayed electives), and compare them to the intended curriculum structure.
Research Environment: Software/Tools:
- Celonis Academic Edition (provided free for educational research).
- Supporting Python libraries (e.g., PM4Py, Pandas) for data preprocessing.

Data:
- Synthetic or de-identified enrolment records reflecting UNSW MIT program structures (such as core/elective courses, prerequisites, and grades).
- Curriculum structure from the official UNSW Handbook.
Novelty and Contribution: .
Expected Outcomes: - A Celonis process model showing actual versus intended student pathways in the MIT program.
- Insights into bottlenecks, common alternative sequences, and risky transitions (e.g., failing a core course or delaying electives).
- A short research report (15–20 pages) summarising methods, results, and recommendations.
- A visual demo dashboard in Celonis that showcases pathway analysis for teaching, advising, or curriculum planning.
Reference Material Links: 1. Van Der Aalst, W. M., & Carmona, J. (2022). Process mining handbook (p. 503). Springer Nature.
2. Celonis Academic Alliance https://www.celonis.com/company/our-programs/academic-alliance
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Router-Free Scalable MoE Language Model: Competitive Arena Performance & Novel MoE Techniques
Name of Supervisor: Flora Salim
Email of Supervisor: flora.salim@unsw.edu.au
Name of Joint/Co-Supervisor: Toan Nguyen
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: This project fine-tunes a Mixture-of-Experts (MoE) language model using the FOGO optimizer. FOGO's spectral orthogonalization of gradient and momentum updates prevents a small set of update directions, and the corresponding experts, from monopolizing optimization. A natural side effect is expert load balancing at the optimizer level, without any auxiliary load-balancing loss or bias term (router-free). The project pursues two parallel goals. The first is to build a strong instruction-tuned MoE chat model that scales well with the number of experts and is competitive on Arena-style leaderboards. The second is to explore novel MoE techniques, including router-free balancing, expert specialization via orthogonalization, and scaling strategies, toward a publication.
Research Environment: CRUISE Lab; HPC GPU cluster (Grid Engine/PBS)
Novelty and Contribution: .
Expected Outcomes: Outcomes(1) An MoE based training/fine-tuning codebase; (2) an instruction-tuned MoE chat model competitive on benchmarks; (3) a novel MoE technique; (4) analysis of expert specialization and load balance; (5) a conference paper submission.
Reference Material Links: FOGO (arXiv:2606.10406) · DeepSeekMoE (arXiv:2401.06066) · OLMoE (arXiv:2409.02060) · Soft-MoE (arXiv:2308.00951) · Autonomy-of-Experts / AoE (arXiv:2501.13074) · LMArena
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: SMT-based verification of Pancake device drivers via Viper
Name of Supervisor: Miki Tanaka
Email of Supervisor: miki.tanaka@unsw.edu.au
Name of Joint/Co-Supervisor: Gernot Heiser
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Embedded Systems and Communications
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Pancake is a research programming language developed at Chalmers University of Technology, ANU, and UNSW. It is developed in the theorem prover HOL4 and comes with a formally verified compiler and is built from the ground up for predictable compilation and ease of verification. It specifically targets verified systems programming.

We have verified some properties of an ethernet driver written in Pancake by annotating the code with necessary conditions and translating it into Viper, an intermediate language, and then feeding it to SMT backends.

The aim of this project is to produce more test cases for this Pancake-to-Viper verification framework and then to compare and evaluate them, with an aim to assess its efficiency and provide data points for further improvements. The verification process involves writing programs (in particular, device drivers) in Pancake, and then add annotations representing pre- and post-conditions of the verification.
Research Environment: The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
Novelty and Contribution: .
Expected Outcomes: - Report outlining the approach taken, tradeoffs considered and work done.
- Pull request to the Trustworthy Systems Group's github repository with implementations.
Reference Material Links: https://trustworthy.systems/projects/pancake/
https://www.pm.inf.ethz.ch/research/viper.html
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Testing and Verification for Neural Networks and LLMs
Name of Supervisor: Yulei Sui
Email of Supervisor: y.sui@unsw.edu.au
Name of Joint/Co-Supervisor: .
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Programming Languages and Software Engineering
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Deep learning models and large language models (LLMs) are increasingly deployed across critical domains such as transport, supply chain, defence, finance, space, and communications. As their decisions directly affect safety and trust, ensuring responsible and reliable AI has become a top priority for both industry and research.

This project focuses on the testing and verification of neural networks and LLMs to evaluate and strengthen their robustness, a core correctness property for trustworthy AI systems. Robustness ensures that small perturbations in inputs do not lead to significant or unexpected changes in outputs. However, existing models often exhibit vulnerabilities such as unstable behaviour, biased outcomes, or privacy leakage, raising concerns about their reliability and fairness.

To address these challenges, the project will combine fuzz testing, for systematically exploring diverse input scenarios and uncovering hidden failure cases, with formal verification techniques to provide stronger guarantees. We will investigate abstract interpretation methods (e.g., ACT) and optimisation-based solvers (e.g., Gurobi) to certify robustness and quantify accuracy variance in deep models. The integration of fuzzing and verification will enable scalable and automated approaches for assessing and improving the trustworthiness of DNNs and LLMs in real-world applications.
Research Environment: Based on the open-source tool: https://github.com/SVF-tools/ACT
Novelty and Contribution: .
Expected Outcomes: Analyzing and verifying modern AI models
Reference Material Links: https://github.com/SVF-tools/ACT
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


Project Title: Wait or Guess?: Improving Large Language Models' Ability for Live Translation
Name of Supervisor: Aditya Josh
Email of Supervisor: aditya.joshi@unsw.edu.au
Name of Joint/Co-Supervisor: Dipankar Srirag
Email of Joint/Co-Supervisor: .
School: School of Computer Science and Engineering
For CSE and EET Projects: School Project
Faculty Research Area (Theme): Intelligent & Autonomous Systems
Applicable to other Engineering
schools/disciplines:
Terms:
Term 2
Abstract: Live machine translation using LLMs (formally referred to as: "Simultaneous Machine Translation") is a challenging task because it involves translating sentences while they are being uttered. Imagine a live translator that hears a person say "I went to the bank". Should the translator anticipate that the word 'bank' is a financial institution? What if the person completes the sentence as "..to catch fish"? While current LLMs 'anticipate' what's coming next, and translate upcoming words before they are spoken, this 'proactive' approach often leads to hallucinations, committing to incorrect translations based on flawed guesses. The project aims to create new methodologies for live machine translation utilising existing neural and statistical models. The team is co-led by Dr. Aditya Joshi, an expert in natural language processing (NLP), and Dipankar Srirag, a PhD student, in the NLP research group.

The ideal student will have strong programming skills in NLP libraries (such as Pytorch, HuggingFace) and NLP/deep learning techniques. Completion of an academic course in NLP (similar to COMP6713 at UNSW) would be highly regarded.
Research Environment: The student will be a part of the natural language processing (NLP) research group consisting of postdocs, software engineers and PhD students. The student will have access to typical computing facilities at UNSW.
Novelty and Contribution: .
Expected Outcomes: 1) Methodology that utilises mechanisms such as uncertainty gating to achieve the tradeoff between speed and accuracy in Simultaneous Machine Translation.
2) Benchmarking on standardised datasets (such as MuST-C).
3) Well-documented code and programmer manuals
4) Report that is in a form suitable for a research paper
Reference Material Links: https://aclanthology.org/2024.alta-1.7.pdf
https://aclanthology.org/2021.emnlp-main.537.pdf
https://aclanthology.org/2024.findings-eacl.15.pdf
https://aclanthology.org/2022.emnlp-main.378.pdf
https://aclanthology.org/2024.iwslt-1.36.pdf
https://aclanthology.org/2025.findings-ijcnlp.138.pdf
https://aclanthology.org/2025.emnlp-main.1191.pdf
https://aclanthology.org/2025.naacl-long.286.pdf

The scope of the project will be broadly based on the reference material above.
Will the student visit the premises of an industry partner, or undertake any activity on premises external to UNSW? No

[Back to Top]


 

Projects offered by other Engineering Schools that may be of interest are:

 

Graduate School of Biomedical Engineering