Skip to main content

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

Research Group Leaders

June Andronick June Andronick Principal Researcher; Conjoint Associate Professor, UNSW

June is leading the Trustworthy Systems research group. Her main research interest is in formal verification and certification of software systems, more precisely in formal proof of correctness and security properties of programs using interactive theorem proving, as well as concurrency reasoning, targeting interruptible and multicore systems.

Research Leaders

Gabriele Keller Gabriele Keller Principal Researcher; Associate Professor, UNSW

Gabriele Keller is interested in Programming Languages. Type Systems, Domain specific languages, and Parallel Computing GPGPU

Gernot Heiser Gernot Heiser Chief Research 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/cyber-physical systems, OS security and robustness issues, general cyber-security, energy/power management, real-time systems, virtualization and architectural support for operating systems.

Gerwin Klein Gerwin Klein Chief Research Scientist; 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.

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 Chief Research Scientist; 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


Carroll Morgan Carroll Morgan Senior Principal Researcher; Professor, UNSW

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

Christine Rizkallah Christine Rizkallah Researcher

Higher-Order Logic - Interactive Theorem Proving - Formal Verification

Johannes Aman Pohjola Research Scientist

Johannes is interested in interactive theorem proving, program verification and concurrency theory.

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." Kai left Data61 in 2018 to join <a href="">COG systems</a>

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 Research Scientist; 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.

Sidney Amani Sidney Amani Research Engineer

Sidney's research focuses on finding practical approaches to formally verify software systems. His current interests include the verification of Ethereum smart contracts and multicore support for seL4. In the past, Sidney worked on Cogent, a purely functional language designed to facilitate the verification of low-level code, which he used to verify a flash file system. He also has experience writing Linux device drivers and static analysis tools.

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; Senior Lecturer, UofA

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

Engineering Staff

Anna Lyons Anna Lyons Senior Research Engineer

Anna is a senior engineer on the seL4 team, taking the role after completing her PhD on the mixed-criticality API and design for seL4. Anna is dedicated to bringing seL4 to the world, by building a strong team of engineers who together build a great platform and community.

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.

Curtis Millar Curtis Millar OS Engineer; Casual Academic

Curtis is interested in improving systems level security through advancements in platform architecture, tooling, and education.

Ed Pierzchalski Ed Pierzchalski Proof Engineer

Ed is a proof engineer working on extending the seL4 proof to more architectures.

Ihor Kuz Ihor Kuz Principal Research Engineer; Conjoint Associate Professor, 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.

Japheth Lim Japheth Lim Proof Engineer

Japheth is interested in automation for software verification. He aims to provide the proof engineering projects in Trustworthy Systems with fast and reliable proof algorithms.

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.

Kent Mcleod Kent Mcleod Research Engineer

Kent is mostly concerned with low-level operating systems and drivers.

Kofi Doku Atuah Kofi Doku Atuah OS Engineer

Microkernels, Drivers, Scalability, Real-time. Kofi cares about coordinating the currently disjoint world of drivers, and unifying the Free and Open Source world and strengthening open-source Operating Systems' ability to work with hardware vendors to get the drivers they need.

Liam O'Connor-Davis Liam O'Connor-Davis Research Engineer

Liam is interested in Programming Languages and Systems, Type Theory, Category Theory, Concurrent and Distributed Systems, Functional Programming and Formal Verification.

Luke Mondy Luke Mondy System Administrator/Computer Systems Support Officer

Luke is a systems administrator and research support tech for the Trustworthy Systems group. He is also currently completing a PhD in computational geodynamics.

Matthew Brecknell Matthew Brecknell Proof Engineer

Matthew is interested in formal verification of software, using mechanised theorem provers. His current challenge is figuring out how to rapidly, yet sustainably evolve large bodies of existing proofs to meet new requirements.

Michael Sproul Proof Engineer

Michael is working on CakeML and seL4 verification as part of the CASE project.

Miki Tanaka Senior Research Engineer

Miki is mainly interested in formal verification techniques and their application to software systems.

Mitchell Buckley Mitchell Buckley Proof Engineer

Mitchell has a formal education in mathematics and a research background in category theory, Hopf algebra and formalised mathematics. He now writes proofs that verify functional correctness of the seL4 micro-kernel.

Pang Luo Pang Luo Proof Engineer

Pang's interests include formal verification and software engineering.

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; Conjoint Senior Lecturer, UNSW

Peter's research interests include operating system algorithms for scalability, especially storage, scheduling, memory management, and locking. He is also interested in systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He contributes to low-level open-source systems tools like QEMU and U-Boot as needed for TS projects.

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.

Siwei Zhuang Siwei Zhuang Research Engineer

Operating System internals, Device drivers and Embedded System Architecture.

Vincent Jackson Proof Engineer

Vincent is interested in proof theory, type theory, and theorem proving.

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.

Amirreza Zarrabi Amirreza Zarrabi PhD Student
Supervised by Kevin Elphinstone

Amir is researching operating system architecture, and multiserver architectures for OS design

Callum Bannister Callum Bannister PhD Student
Supervised by Rafal Kolanski

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

Hira Syeda Hira Syeda PhD Student
Supervised by Rafal Kolanski

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

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.

Robert Sison Robert Sison PhD Student
Supervised by Michael Norrish

Robert is broadly interested in discovering how one may design and construct large systems with formally proved information-flow security properties. His current research focus is on the development and improvement of formal methods for the preservation of information-flow security properties across compilation.

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

Kenny Lau
Supervised by Ihor Kuz

Served by Apache on Linux on seL4.