Trustworthy Systems

Quick links: Alumni Research Group Leader, Academic Staff, Engineers and Research Assistants, Research Students, Coursework Students, Summer Students, Support, Affiliates

Research Group Leader

Gernot Heiser Gernot Heiser  Scientia Professor; John Lions Chair

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.

Academic Staff

Carroll Morgan Carroll Morgan  Professor

Carroll's research is on formal methods, semantics, security, program correctness and probability.

Craig McLaughlin Craig McLaughlin  Research Associate

Craig's research interests include type theory, logic, programming languages, compilers, and formal verification.

Johannes Åman Pohjola Johannes Åman Pohjola  Lecturer

Johannes is interested in beauty and truth. Specifically, he works on interactive theorem proving, program verification and concurrency theory.

Kevin Elphinstone Kevin Elphinstone  Associate Professor

Kevin works on operating system microkernels 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.

Scott Buckley Scott Buckley  Research Associate

Scott works in the time protection team.

Zoltan Kocsis Zoltan Kocsis  Research Associate

Zoltan, a non-standard analyst by training, works on the correctness proof for the seL4 kernel.

Engineers and Research Assistants

Alwin Joshy Alwin Joshy  Research Assistant

Alwin is working on optimising the IRQ and Exception fast paths in seL4.

Andy Bui Andy Bui  Research Assistant

Andy is working on improving the device driver framework.

Courtney Darville Courtney Darville  Research Assistant

Courtney works on secure multi-server operating system design.

Ivan Velickovic Ivan Velickovic  Research Assistant

Ivan is currently working to improve device drivers on seL4.

James Archer James Archer  Research Assistant

James is working to improve the locking in multicore seL4.

Jingyao Zhou Jingyao Zhou  OS Engineer

Jingyao is interested in real-time operating systems and hardware.

Lucy Parker Lucy Parker  Research Assistant

Lucy is working on the Device Driver Framework, to optimise device drivers running on seL4.

Miki Tanaka Miki Tanaka  Senior Proof Engineer

Miki is interested in formal verification techniques and their application to software systems, and broadly proof engineering as a discipline. Miki has contributed to the verification of architecture porting for seL4 and also the verification of the seL4 MCS extensions as the technical lead. Miki is currently involved in a project for device driver verification using the Pancake language (based on cakeML/HOL4).

Peter Chubb Peter Chubb  Senior Systems Consultant

Peter's research interests include operating system abstractions for, intra alia, storage, scheduling, memory management, and locking. He is also interested in capacity planning, and in systems performance measurement and optimisation. His main expertise is in Unix and Linux kernels, and low level system support built on these. He also maintains the Trustworthy Systems website and internal infrastructure.

Tiana Tsang Ung Tiana Tsang Ung  Research Assistant

Tiana is investigating a new systems language, 'pancake'.

Research Students

Kevin Tran Kevin Tran  PhD Student
Supervised by Johannes Åman Pohjola

Kevin's research is on creating a framework for reasoning about concurrent programs, with the ultimate goal of verifying multicore seL4.

Zilin Chen Zilin Chen  PhD Student; UNSW
Supervised by Gernot Heiser

Zilin's research is into functional programming, type theory, formal verification, compilers, and Embedded DSLs.

Coursework Students

Mitchell Johnston Mitchell Johnston  Honours Thesis Student
Supervised by Gernot Heiser

Mitchell is working on improving the seL4 Mixed-Criticality kernel model, with the aim to create a system with strong temporal isolation properties.

Patrick Hao Patrick Hao  Honours Thesis Student
Supervised by Gernot Heiser

Patrick is working on applying seL4 to the automotive space.

Thomas Bove Thomas Bove  Honours Thesis Student
Supervised by Gernot Heiser

Tom is working on hardware implementations of time protection.

Summer Students

Ben Nott  Summer Student
Supervised by Johannes Åman Pohjola

Logic and automated theorem proving, metamathematics, programming language theory and formal methods.

Krishnan Winter  Summer Student
Supervised by Johannes Åman Pohjola

Krishnan is working with Johannes on the pancacke language.

Mathieu Paturel Mathieu Paturel  Summer Student
Supervised by Zoltan Kocsis

formal methods


Birgit Brecknell Birgit Brecknell  Project Manager

Birgit works part time with the TS group as project manager for strategic and external projects

Christopher Irving Christopher Irving  Administrator

Christopher is helping support the computer systems for the Trustworthy Systems group.

Tessa Lunney Tessa Lunney  Administrator

Tessa works part-time as the Administrative Assistant, managing the office. She works Mondays, Thursdays, and Fridays.


Gerwin Klein Gerwin Klein  Conjoint Professor; Founder and Chief Scientist at Proofcraft

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

Ihor Kuz Ihor Kuz  Conjoint Associate Professor; Engineer at Kry10

Ihor worked at TS from 2003 until 2021. During that time he led the systems team and many of the projects TS was involved with. He now works as an Engineer at Kry10.

Ihor's research interests include operating systems and distributed systems. In particular the design of flexible and modular operating systems, security and safety properties of such systems, distributed system middleware, and management of distributed resources.

June Andronick June Andronick  Conjoint Professor; Founder and CEO at Proofcraft

June had joined the Trustworthy Systems research group in 2008 (in NICTA), and led the group from end of 2016 to end of 2020. 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.

Rafal Kolanski Rafal Kolanski  Conjoint Lecturer; Founder at Proofcraft

Rafal worked as a proof engineer at Trustworthy Systems until April 2021. He led the Proof Engineering team from 2016 until 2021.

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  Visiting Fellow; Research Fellow, University of Melbourne

Robert is broadly interested in discovering how best to design and construct software systems with formally proved functional-correctness and security properties at scale. Their current research concerns the formal verification of operating systems to enforce increasingly useful forms of information-flow security, also known as confidentiality.