Research
Software Systems

Quick links: Research Group Leaders, Research Leaders, Researchers, Technical Support Staff, Research Students, Coursework Students, Student Interns and Visitors, Visitors

Research Group Leaders

Gernot Heiser Gernot Heiser Senior Principal Researcher; Scientia Professor and John Lions Chair, UNSW

Gernot's main research interests are in operating systems, especially microkernel-based systems, and their use in embedded systems, OS security and robustness issues, energy/power management, real-time systems and virtualization. Other interests include computer architecture, especially architectural support for operating systems.

Liming Zhu Liming Zhu Prinicipal Researcher ; Conjoint Academic, UNSW

Liming's research interests include software architecture, dependable systems and operations, DevOps, software ecosystems and service/cloud engineering.

Research Leaders

Alan Fekete Alan Fekete Senior Principal Researcher; Professor, USyd

Software engineering, enterprise systems, cloud computing

Carroll Morgan Carroll Morgan Senior Principal Researcher; Professor, UNSW

Formal methods; semantics; security; program correctness; probability.

Gabriele Keller Gabriele Keller Principal Researcher; Associate Professor, UNSW

Programming Languages Type Systems Domain specific languages Parallel Computing GPGPU

Gerwin Klein Gerwin Klein Senior Principal Researcher; Conjoint Professor, UNSW

Gerwin's research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, and semantics of programming languages. Generally, he wants software systems to be dependable, and thinks that formal specification and proof can make a very significant contribution towards that goal.

Guido Governatori Guido Governatori Senior Principal Researcher; Adjunct Professor, Queensland University of Technology

Guido's research interests include non-classical logics, non-monotonic reasoning, formal models of normative reasoning, and their applications to business process modelling. A basic guideline of my research is to investigate conceptually sound formal models and methods grounded on understood principles of the underlying (application) phenomena, and with the aim of providing logic-based computationally oriented solutions.

John Grundy John Grundy Senior Principal Researcher; Professor of Software Engineering and Dean, School of Software and Electrical Engineering, Swinburne University of Technology

software methods and tools automated software engineering model-driven engineering software security engineering visual languages and tools user interfaces software engineering education

Kevin Elphinstone Kevin Elphinstone Principal Researcher; Associate Professor, UNSW

Small operating system kernels and the infrastructure required to support larger systems upon them. His current focus includes secure embedded operating systems suitable for formal verification, and for being the basis of secure systems for embedded devices. He also has interests in componentised operating systems, operating systems in general, security, real-time systems, computer architecture as it pertains to operating systems, and virtualisation.

Mark Staples Mark Staples Principal Researcher; Conjoint Senior Lecturer, UNSW

Mark's research interests are in software engineering. His current research focuses on three areas: software architecture for secure embedded systems; empirical software engineering research for formal verification projects; and the validity of models in formal methods. More general research interests include software configuration management, software architecture, software product line development, and software process improvement.

Peter Baumgartner Peter Baumgartner Principal Researcher; Adjunct Associate Professor, ANU

Advancement of automated deduction, in particular first-order logic theorem proving; applications for software verification, knowledge representation, and business rules/process analysis; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.

Ralf Huuck Ralf Huuck Principal Researcher

Ralph is a project leader in the Software Systems Group at NICTA and heads the research and development of the Goanna tool that combines model checking with static analysis for C/C++ source code analysis. Goanna is available commercially as well as for academic use.

Robert van Glabbeek Robert van Glabbeek Senior Principal Researcher; Conjoint Professor, UNSW

Rob strives to create and study comprehensive models and theories of concurrent processes, thereby answering fundamental questions such as: which problems can be solved in a distributed way, using only asynchronous communication, and which cannot. These insights are applied to the modelling, verification and analysis of distributed systems, in particular to popular routing protocols in wireless mesh networks.

Researchers

Abderrahmane Maaradji Abderrahmane Maaradji Researcher

Process mining, sequence mining, BPM

Badiul Islam Badiul Islam Researcher

Artificial Intelligence, Defeasible Logic, Knowledge Representation, Business Process Compliance, Legal Representation, Privacy, Social Media and Web 2.0

Brian Lam Brian Lam Researcher

Brian's research interests include non-monotonic reasoning, formal models of normative reasoning, and their applications. A basic guideline of my research is to improve the computational complexity of defeasible reasoning (with different variants) and their applications in different domains, such as UAV navigation, business process compliance, etc.

Christine Rizkallah Christine Rizkallah Researcher; Conjoint Lecturer, UNSW

Higher-Order Logic Interactive Theorem Proving Software Verification

Daniel Sun Daniel Sun Researcher; Conjoint Lecturer, UNSW

Big Data, Data analytics and software, Cloud Computing, Software system reliability, Energy Efficiency, Networking, Cyber Security

Ingo Weber Ingo Weber Senior Researcher; Adjunct Senior Lecturer at UNSW

Ingo's research interests include Cloud computing, Systems Operations, Business Process Management, and Artificial Intelligence / AI Planning.

June Andronick June Andronick Senior Researcher; Conjoint Senior Lecturer, UNSW

June's main research interest is in formal verification and certification of software systems, and more precisely in formal proof of correctness and security properties of programs using interactive theorem proving.

Kai Engelhardt Kai Engelhardt Senior Researcher; Senior Lecturer, UNSW

Kai's research mostly attempts to refute the third sentence of the following proverb of unknown (?) origin. "The problem with engineers is that they cheat in order to get results. The problem with mathematicians is that they work on toy problems in order to get results. The problem with program verifiers is that they cheat on toy problems in order to get results."

Kopal Kapoor Kopal Kapoor Researcher; Program Manager

The interface of regulation/law and IT.

Leonid Ryzhyk Leonid Ryzhyk Researcher

Leonid's research interests are centred around the use of formal techniques for building better operating systems.

Marcello La Rosa Marcello La Rosa Principal Researcher; Professor

Marcello's research interests embrace different topics in the area of Business Process Management (BPM), such as process mining, management of process variability and process model collections, process automation and risk-aware BPM.

Michael Norrish Michael Norrish Principal Researcher

Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.

Nick van Beest Researcher

Paul Bannerman Paul Bannerman Researcher

Paul's research interests include software and systems technology adoption and utilisation (such as cloud computing), risk management, project management, software engineering governance, organisational capabilities in software engineering and the alignment of software engineering practices with organisational needs and objectives. He supervises thesis students (Masters and PhD) in these and related research areas.

Peter Höfner Peter Höfner Senior Researcher; Conjoint Senior Lecturer

Peter's research interests are Formal Methods, more specifically he is interested in methods for describing software systems, in particular distributed and concurrent systems such as routing protocols or hybrid systems. For analysing and verifying these techniques he uses algebraic techniques such as process algebra and semirings. Moreover he tries to use off-the-shelf verification tools (automated theorem provers, model checkers) to automate the developed approaches.

Ralph Holz Ralph Holz Researcher; Conjoint Lecturer, UNSW; Associate Member of Chair, TUM

My research interests revolve around the general topic of (network) security.

Regis Riveret Researcher; Researcher

My research programme focuses on the conception and implementation of a probabilistic rule-based argumentation framework to study (self) norm-governed learning agents. The framework has a layered architecture dealing with: (i) rule-based argumentation (ii) probabilistic argumentation (iii) learning and strategy (iv) norm-governed multi-agent systems (v) self-organisation. I am also particularly interested in applications in legal informatics and simulations in social-sciences.

Sherry Xu Sherry Xu Researcher

Sherry (Xiwei Xu) is interested in software architecture, including architecture adaptation, evolution, quality attributes, and business process, including modeling, adaption, and management. Her current research topics include cloud computing, system operation, dependability etc.

Toby Murray Toby Murray Senior Researcher; Conjoint Senior Lecturer, UNSW

Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems.

Vincent Gramoli Vincent Gramoli Senior Researcher; Senior Lecturer, University of Sydney

Vincent's research interest is in concurrency, including distributed applications and synchronization.

Yuval Yarom Researcher; Research Associate, UofA

Yuval's main research interests are computer security and cryptography, with a current focus on side-channel attacks and defences.

Technical Support Staff

Adnene Guabtni Adnene Guabtni Senior Research Engineer

Adnene's research interests include Service Oriented Computing, Business Process Management, Cloud Computing, Business Intelligence, Software Engineering and Web Information technologies.

Adrian Danis Adrian Danis Research Engineer

Adrian is interested in the development of operating systems, especially when it involves micro-kernels, Intel architecture and virtualization.

Alex Hixon Research Assistant

Alex's research interests include: parallel computing; alternative computer architectures (looking ahead to the plateau of Moore's Law); applications of formal methods on software systems; as well as operating system and kernel design.

An Binh Tran An Binh Tran Research Assistant

Dependable Cloud, DevOps, Big Data

Chao Li Chao Li Software Engineer

DevOps, Distributed Systems, Cloud Computing.

Corey Lewis Corey Lewis Research Engineer

Corey's research interests include formal methods, functional programming and program verification. He is also interested in mathematically analysing graph models of large real world networks.

Felix Kam Felix Kam Research Assistant

Felix's research interests include operating system design, embedded systems in general and formal methods, particularly interactive theorem proving.

Ihor Kuz Ihor Kuz Senior Research Engineer; Conjoint Senior Lecturer, UNSW

Ihor's research interests include operating systems and distributed systems. With regards to operating systems, he focuses on the design of flexible and modular operating systems, as well as security and safety properties of such systems. In distributed systems, he is interested in distributed system middleware, supporting services, and management of distributed resources.

Ingo Mueller Ingo Mueller Software Engineer Cyber Security

Ingo's research interests include information security and secure software development.

Joel Beeren Joel Beeren Research Engineer

Joel's research interests include the application of formal mathematical principles (especially number theoretic concepts) to computing design, as well as the use of formal methods in operating systems.

John Judge John Judge Senior Research Engineer

Dr John Judge is a senior research engineer in SSRG and works with the Broadband and Digital Economy business group. His research interests include and home and zeroconf networking.

Mark Bradley Research Engineer/Scientist

Mark is interested in the processes and methods of software verification that are practical for end users.

Peter Chubb Peter Chubb Principal Research Engineer; Conjoint Senior Lecturer, UNSW

Peter's research interests include operating system algorithms for scalability, including storage, scheduling, memory management, and locking. He is also interested in systems performance measurement and optimisation.

Rafal Kolanski Rafal Kolanski Senior Research engineer

Rafal is interested in the verification of system-level software, particularly software involving virtual memory such as operating systems. He is very interested in separation logic and the possibilities it creates for making this verification task easier.

Robert Sison Robert Sison Research Assistant

Robert's primary research interest is to discover how one may prove information flow properties in a compositional manner, and thereby design and construct large systems with formally proven information flow properties.

Siwei Zhuang Siwei Zhuang Research Assistant

Operating System internals, Device drivers and Embedded System Architecture.

Stephen Sherratt Stephen Sherratt Research Engineer

Stephen's research interests include operating systems, virtualization and device drivers.

Xin Gao Xin Gao Research Engineer

symbolic computation and fourier analysis.

Yutaka Nagashima Yutaka Nagashima Research Assistant

Yutaka's research interests include proof assistants, concurrent and parallel programming.

Zilin Chen Zilin Chen Research Assistant

Functional programming, type theory, compilers, Embedded DSLs.

Research Students

Aaron Carroll Aaron Carroll PhD Student
Supervised by Gernot Heiser

Aaron works on smartphone energy management, and is primarily interested in how multi-core applications processors can be used to reduce energy consumption when combined with well-established techniques such as frequency/voltage scaling. He also works on understanding how energy is consumed within smartphones, using physical instrumentation and measurement on real-world devices. Recently, Aaron has been exploring techniques which exploit multi-core CPUs to improve sequential performance.

Adam Christopher Walker Adam Christopher Walker PhD Student
Supervised by Leonid Ryzhyk

Adam is interested in using formal techniques to synthesize device drivers from existing device specifications. This approach will dramatically reduce the number of operating system faults caused by drivers as well as driver development time.

Adel Alqahtani Adel Alqahtani PhD Student
Supervised by Liming Zhu

Cloud Computing, Software Defined Networking.

Alexander Kroh Alexander Kroh PhD Student
Supervised by Peter Chubb

Embedded systems; Computer architecture; Devices and device drivers.

Alexander Legg Alexander Legg PhD Student
Supervised by Leonid Ryzhyk

Alex is currently working on improving the performance of device driver synthesis by applying results from the satisfiability community. His interests lie in the area of applying formal methods to real world problems.

Anna Lyons Anna Lyons PhD Student
Supervised by Gernot Heiser

Anna is a PHD student working on converting seL4 to a real-time operating system for mixed-criticality systems. An example of a mixed-criticality system is a autonomous helicopter. To do this, seL4 requires a real-time scheduler with mixed-criticality support, a real-time API, primitives for trusted real-time locking, and capabilities for managing CPU time.

Bin Liu Bin Liu PhD Student; To be PhD Student
Supervised by Liming Zhu

Bin is interested in Cloud Computing, Security of cluster application ecosystems, LXC, Docker, Distributed Systems and Network Modelling.

Daniel Matichuk Daniel Matichuk PhD Student
Supervised by Gerwin Klein

Daniel is interested in interactive theorem provers and proof automation. His current work is in increasing the scalability and maintainability of formal machine-checked proofs through refactoring.

Dongyao Wu Dongyao Wu PhD Student
Supervised by Liming Zhu

Distributed Systems, Big Data Processing, Parallel Computing, Cloud Computing, Machine Learning

Jan-Christoph Kuester Jan-Christoph Kuester PhD Student
Supervised by Peter Baumgartner

Jan's research interests include runtime verification, (first order) temporal logics, automata theory, formal methods, software and systems engineering for safety and security critical embedded systems, and especially android security.

Joshua Bax Joshua Bax PhD Student
Supervised by Peter Baumgartner

Josh's research area is Automated Reasoning, in particular with First-Order Logic applied to finite domains and data structures typically found in verification of software systems.

Mansour Khelghatdoust Mansour Khelghatdoust PhD Student
Supervised by Daniel Sun

Distributed Computing, Cloud Computing

Matthew Fernandez Matthew Fernandez PhD Student
Supervised by Ihor Kuz

Matthew's research interests are in the application of formal methods to large software systems, and in componentised systems and proofs.

Matthew Sladescu Matthew Sladescu PhD Student
Supervised by Anna Liu

Adaptive and Self Managing Systems; Cloud Computing; Software Architecture, and User Interface Design

Min Fu Min Fu PhD Student
Supervised by Liming Zhu

Cloud Computing, Software Architecture, Software Engineering, Systems Analysis, Object-Oriented Programming

Mohammad Abdulaziz Mohammad Abdulaziz PhD Student
Supervised by Michael Norrish

I am interested in Interactive theorem proving. My PhD project is about mechanizing optimality properties in SAT based planning algorithms.

Mostafa Farshchi Mostafa Farshchi PhD Student
Supervised by John Grundy

Cloud Dependability, Cloud Process Operations, Process Mining.

Mustafa Hashmi Mustafa Hashmi PhD Student
Supervised by Guido Governatori

I am interested in Automation and Analysis of Business Process, Business Rules Compliance Management, Defeasible Logic, Non-monotonic Reasoning and their applications to solve complex problems in Large Scale Enterprises.

Nazrina Khurshid Nazrina Khurshid PhD Student
Supervised by Paul Bannerman

Software development process improvement, sustainment model, systems adoption and development of organisational capabilities

Paul Rimba Paul Rimba PhD Student
Supervised by Liming Zhu

Paul's research interests include security, software architecture, security patterns, capability-based systems and application design.

Qian Ge Qian Ge PhD Student
Supervised by Gernot Heiser

Qian is a second year PhD student who is working on eliminating timing side channels from seL4 with lightweight countermeasures. Qian is supervised by Prof. Gernot Heiser and Dr. Kevin Elphinstone.

Rabia Chaudry Rabia Chaudry PhD Student
Supervised by Adnene Guabtni

Continuous availability, predictive analysis, machine learning, decision support systems.

Sidney Amani Sidney Amani PhD Student
Supervised by Toby Murray

Sidney's research focuses on finding a practical approach to make file systems amenable to a functional correctness proof formalised in an interactive theorem prover. His previous research includes developing a framework to automatically verify device drivers interactions with the rest of the operating system.

Teuku Geumpana Teuku Geumpana PhD Student
Supervised by Liming Zhu

Cloud computing, dependable cloud, mobile cloud computing

Thomas Sewell Thomas Sewell PhD Student
Supervised by Gerwin Klein

Thomas is interested in program verification, programming languages and operating systems. His PhD thesis is to prove that compilation preserves the properties proved of the source code in projects such as L4.verified.

Yanyan Shen Yanyan Shen PhD Student
Supervised by Kevin Elphinstone

Yanyan is currently researching how to improve the trustworthiness of commodity hardware through software to enable the verified microkernel to be used in situations previously needing an air gap. Multi-core processors are used to provide redundancy and cross-core checking is employed to detect divergence caused by hardware faults. The aim is to increase the trustworthiness of a virtual air gap created by the microkernel, and thus systems running on COTS hardware.

Coursework Students

Joseph Tuong Joseph Tuong Honours Thesis Student
Supervised by June Andronick

Formal methods, high-assurance systems and programming language theory & design.

Student Interns and Visitors

James Zheng James Zheng Local Visiting Student; PhD Candidate, University of Texas at Austin
Supervised by Gernot Heiser

His current research focuses on the design and implementation of middlewares for cyber physical systems (CPS), including looking into model-driven development for fast prototyping of CPS and various way (especially formal methods) to aid verification and validation of mission-critical CPS.

Jan Auer Jan Auer Overseas Visiting Intern
Supervised by Ralf Huuck

Jan currently conducts research on runtime verification for static code analysis tools for his Master's thesis at the TU Munich, Germany.

Japheth Lim Japheth Lim Intern
Supervised by Christine Rizkallah

Shanush Prema Thasarathan Shanush Prema Thasarathan Intern; Undergraduate @ UNSW - BE ME Electrical Engineering
Supervised by Peter Chubb

Suhrid Satyal Overseas Visiting Intern
Supervised by Ingo Weber

Cloud Computing, Dependable Systems, Web Services

Yu Ma Yu Ma Overseas Visiting Intern
Supervised by Ingo Weber

Cloud Computing

Visitors

Anna Liu Anna Liu Visiting Researcher

Software Engineering, Distributed Systems, Performance Engineering, Middleware and Cloud Architectures

Antony Hosking Antony Hosking Visiting Researcher; Associate Professor, Purdue

runtime systems, memory management, transactional memory

Hiroshi Wada Hiroshi Wada Visiting Senior Researcher; Conjoint Senior lecturer, UNSW

Hiroshi's research interests include distributed computing, performance engineering, biologically-inspired computing and model-driven software engineering.

Len Bass Len Bass Visiting Researcher; Conjoint Professor, UNSW

My research interests center around software architecture and its applications. Over the years, this has ranged from architecture evaluation, design, and documentation to supporting usability through software architecture to requirements elicitation to help define the software architecture to global software development to defining architecture related security controls for the smart grid. Currently, I am interested in the problem of creating trusted connectors within an architecture.

Liang Zhao Liang Zhao Visiting Research Engineer

My research interest is on the general area of deploying data-intensive applications on cloud environments. In particular, trade-offs (e.g. performance, scalability, and data consistency) of the different approaches of hosting the database tier (e.g. DaaS, NoSQL systems, virtualized database servers) of software applications in public cloud platforms. aiming of bridging the gaps between the SLA requirements of consumer applications and the SLA guarantees of cloud providers.

Qinghua Lu Qinghua Lu Visiting Researcher

Qinghua's interest includes cloud computing, business-driven IT management, autonomic computing, IT system and service management, and service-oriented computing.

Ross Jeffery Ross Jeffery Visiting Researcher; Emeritus Professor, UNSW

Ross' current research interests lie in software development process modelling and improvement, software cost modelling and estimation, software metrics and systems adaptation.