Skip to main content


Quick links: Research Group Leaders, Research Leaders, Researchers, Engineering Staff, Research Students

Research Group Leaders

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.

Research Leaders

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

Gernot Heiser Gernot Heiser Chief Principal Scientist; 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, general cyber-security, energy/power management, real-time systems and virtualization. Other interests include computer architecture, especially architectural support for operating systems.

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.

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.

Rob van Glabbeek Rob 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.

Tony Hosking Tony Hosking Contributed Researcher; Professor, ANU

runtime systems, memory management (garbage collection), transactional memory


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

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.

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

Ramana Kumar Ramana Kumar Researcher

Ramana is interested in building systems with end-to-end functional correctness theorems, and in techniques for interactive theorem proving. He is a developer of CakeML, a verified ML-like programming language (i.e., language spec, and compiler and runtime), and wants to verify the combined system consisting of CakeML running on the seL4 verified OS. Ramana's long-term interest is ensuring that, when computer systems become substantially more powerful, their impact is beneficial.

Toby Murray Toby Murray Senior Researcher; Lecturer, University of Melbourne

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

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.

Engineering Staff

Adrian Danis Adrian Danis Senior Research Engineer

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

Anna Lyons Anna Lyons Research Engineer

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.

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.

Daniel Matichuk Daniel Matichuk Research Engineer

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.

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.

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.

Kalana Gamlath Kalana Gamlath Research Engineer

Kalana's research interests include operating systems, trusted component systems, and safe automotive systems.

Kofi Doku Atuah Kofi Doku Atuah OS Engineer

Microkernels, Drivers, Scalability, Real-time.

Luke Mondy Luke Mondy System Administrator/Computer Systems Support Officer

System administration

Maksym Bortin Maksym Bortin Proof Engineer

formal software development, software verification, formal reasoning

Matthew Brecknell Matthew Brecknell Proof Engineer

Matthew is interested in functional programming, type theory, and formal verification by theorem proving.

Partha Susarla Ajay Partha Susarla Ajay OS Engineer

Partha's research interests include Operating Systems, File Systems, Multimedia codecs and Distributed computing.

Peter Chubb Peter Chubb Principal Research Engineer; Adjunct 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 formal verification of high assurance, system-level software, both from the perspective of verification in practice, but also proof maintenance and increasing the proof coverage of already verified systems.

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.

Seb Holzapfel Seb Holzapfel Research Assistant

Sebastian is interested in low level & embedded systems, RTOS development & hardware design.

Shanush Prema Thasarathan Shanush Prema Thasarathan Intern; Undergraduate @ UNSW - BE ME Electrical Engineering

Sidney Amani Sidney Amani Research Engineer

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.

Siwei Zhuang Siwei Zhuang Research Engineer

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.

Yutaka Nagashima Research Assistant

Yutaka's research interests include proof assistants and proof automation.

Zilin Chen Zilin Chen Research Engineer; PhD Student, UNSW

Functional programming, type theory, compilers, Embedded DSLs.

Research Students

Alexander Kroh Alexander Kroh PhD Student
Supervised by Kevin Elphinstone

Embedded systems; Computer architecture; Devices and device drivers.

Callum Bannister Callum Bannister PhD Student
Supervised by Michael Norrish

Callum's research interests are in functional programming and formal verification. His current work is in separation logic.

Hira Syeda Hira Syeda PhD Student; PhD Student
Supervised by Rafal Kolanski

Hira is a first year PhD student and is working on developing a Unified Memory Model for kernel's verification. Her interests include interactive theorem proving, software verification and embedded systems. Hira is supervised by Prof. Gerwin Klein and Dr. Kevin Elphinstone.

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.

Qian Ge Qian Ge PhD Student
Supervised by Kevin Elphinstone

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

Thomas Sewell Thomas Sewell PhD Student
Supervised by Rafal Kolanski

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.